expChar_pow_pos — Mathlib

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)

Похожие утверждения