Step
*
1
of Lemma
rinv1
.....antecedent.....
rnonzero(r1)
BY
{ (D 0 With ⌜3⌝ THEN Auto) }
Latex:
Latex:
.....antecedent.....
rnonzero(r1)
By
Latex:
(D 0 With \mkleeneopen{}3\mkleeneclose{} THEN Auto)
Home
Index