---

Step * of Lemma qinverse_q

No Annotations
∀[a:ℚ]. (((a + -(a)) = 0 ∈ ℚ) ∧ ((-(a) + a) = 0 ∈ ℚ))
BY
{ (ProveSpecializedLemmaWReduce grp_inverse)  0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  (((a  +  -(a))  =  0)  \mwedge{}  ((-(a)  +  a)  =  0))


By

---

Latex:
(ProveSpecializedLemmaWReduce  grp\_inverse)    0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}

---

Home Index