spec — Mathlib

English

For any natural x, (x : R) = 0 iff ringChar R divides x.

Русский

Для любого x ∈ ℕ, x в R равен нулю тогда и только тогда, когда ringChar R делит x.

LaTeX

$$$\forall x \in \mathbb{N}, \ (x : R) = 0 \iff \operatorname{ringChar}(R) \mid x.$$$

Lean4

theorem spec : ∀ x : ℕ, (x : R) = 0 ↔ ringChar R ∣ x :=
  by
  letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1
  exact CharP.cast_eq_zero_iff R (ringChar R)

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