eq — Mathlib · SciLib

English

For all a ∈ ℤ, (a : R) = 0 iff p ∣ a, where R has CharP p.

Русский

Для всех a ∈ ℤ, (a : R) = 0 тогда и только тогда, когда p делит a, если R имеет CharP p.

LaTeX

$$$(a : R) = 0 \iff p \mid a.$$$

Lean4

theorem eq {p q : ℕ} (hp : CharP R p) (hq : CharP R q) : p = q :=
  Nat.dvd_antisymm ((cast_eq_zero_iff (self := hp) R p q).1 (@cast_eq_zero _ _ _ hq))
    ((cast_eq_zero_iff (self := hq) R q p).1 (@cast_eq_zero _ _ _ hp))

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