Step
*
2
of Lemma
rinv1
1. (r1 * rinv(r1)) = r1
⊢ rinv(r1) = r1
BY
{ (slowRNorm (-1) THEN Auto) }
1
1. (r1 * rinv(r1)) = r1
⊢ rnonzero(r1)
Latex:
Latex:
1. (r1 * rinv(r1)) = r1
\mvdash{} rinv(r1) = r1
By
Latex:
(slowRNorm (-1) THEN Auto)
Home
Index