---

Step * of Lemma qexp-zero

∀[r:ℚ]. (r ↑ 0 = 1 ∈ ℚ)
BY
{ (InstLemma `exp_zero_q` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  (r  \muparrow{}  0  =  1)


By

---

Latex:
(InstLemma  `exp\_zero\_q`  []  THEN  Trivial)

---

Home Index