---

Step * of Lemma qmul_one_qrng

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  (((a  *  1)  =  a)  \mwedge{}  ((1  *  a)  =  a))


By

---

Latex:
(ProveSpecializedLemmaWReduce  rng\_times\_one)    0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}

---

Home Index