---

Step * of Lemma qinv_id_q

No Annotations
-(0) = 0 ∈ ℚ
BY
{ (ProveSpecializedLemmaWReduce grp_inv_id) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ }

---

Latex:

---

Latex:
No  Annotations
-(0)  =  0


By

---

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

---

Home Index