expChar_one_of_char_zero — Mathlib

English

If the base ring has characteristic zero, then the exponential characteristic equals 1.

Русский

Если характеристика кольца нулевая, то экспоненциальная характеристика равна 1.

LaTeX

$$$[CharZero R] \\\\Rightarrow \\\\ExpChar R q \\\\Rightarrow q = 1$$$

Lean4

/-- The exponential characteristic is one if the characteristic is zero. -/
theorem expChar_one_of_char_zero (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q] : q = 1 :=
  by
  rcases hq with q | hq_prime
  · rfl
  · exact False.elim <| hq_prime.ne_zero <| ‹CharP R q›.eq R hp

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