---

Step * of Lemma qmul_zero_qrng

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

---

Latex:

---

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


By

---

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

---

Home Index