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))