expChar_is_prime_or_one — Mathlib

English

The exponential characteristic is either a prime or equal to 1.

Русский

Экспоненциальная характеристика либо простая, либо равна единице.

LaTeX

$$$\\\\forall R q \\\\[ExpChar R q] \\\\Rightarrow \\\\text{Nat.Prime}(q) \\\\lor q = 1$$$

Lean4

/-- The exponential characteristic is a prime number or one.
See also `CharP.char_is_prime_or_zero`. -/
theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 := by
  cases hq with
  | zero => exact .inr rfl
  | prime hp => exact .inl hp

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