English
Every power of the exponential characteristic is positive: for any n, 0 < q^n when ExpChar R q.
Русский
Любая степень экспоненциальной характеристики положительна: для любого n, 0 < q^n при ExpChar R q.
LaTeX
$$$\\\\forall R q n, \\\\[ExpChar R q] \\\\Rightarrow 0 < q^n$$$
Lean4
/-- Any power of the exponential characteristic is positive. -/
theorem expChar_pow_pos (q : ℕ) [ExpChar R q] (n : ℕ) : 0 < q ^ n :=
Nat.pow_pos (expChar_pos R q)