char_ne_zero_of_finite — Mathlib

English

The characteristic of a finite ring cannot be zero.

Русский

Характеристика конечного кольца не может быть нулём.

LaTeX

$$p ≠ 0$$

Lean4

/-- The characteristic of a finite ring cannot be zero. -/
theorem char_ne_zero_of_finite (p : ℕ) [CharP R p] [Finite R] : p ≠ 0 :=
  by
  rintro rfl
  haveI : CharZero R := charP_to_charZero R
  exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

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