expChar_pos — Mathlib

English

The exponential characteristic is positive: if ExpChar R q, then q > 0.

Русский

Экспоненциальная характеристика положительна: если ExpChar R q, то q > 0.

LaTeX

$$$\\\\forall R q \\\\[ExpChar R q], \\\\ 0 < q$$$

Lean4

/-- The exponential characteristic is positive. -/
theorem expChar_pos (q : ℕ) [ExpChar R q] : 0 < q :=
  by
  rcases expChar_is_prime_or_one R q with h | rfl
  exacts [Nat.Prime.pos h, Nat.one_pos]

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