Step
*
of Lemma
rinv-mul-as-rdiv
∀[y,a:ℝ]. (rinv(y) * a) = (a/y) supposing y ≠ r0
BY
{ (Unfold `rdiv` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[y,a:\mBbbR{}]. (rinv(y) * a) = (a/y) supposing y \mneq{} r0
By
Latex:
(Unfold `rdiv` 0 THEN Auto)
Home
Index