Step
*
of Lemma
rmul-rdiv-one
∀[a,b:ℝ]. (((r1/a) * (r1/b)) = (r1/a * b)) supposing (b ≠ r0 and a ≠ r0)
BY
{ Auto }
Latex:
Latex:
\mforall{}[a,b:\mBbbR{}]. (((r1/a) * (r1/b)) = (r1/a * b)) supposing (b \mneq{} r0 and a \mneq{} r0)
By
Latex:
Auto
Home
Index