English
Let R be a commutative ring with CharP n and I an ideal of R. Then CharP (R/I) n holds if and only if for every natural number x, if the natural x mapped into R lies in I, then x maps to 0 in R.
Русский
Пусть R — коммутативное кольцо с CharP n и I — идеал R. Тогда CharP(R/I) n эквивалентно тому, что для всякого натурального числа x, если образ x в R принадлежит I, то x отображается в ноль в R.
LaTeX
$$$\\mathrm{CharP}(R/I)\\; n \\iff \\forall x\\in\\mathbb{N},\\ (x\\colon R)\\in I \\rightarrow (x\\colon R)=0$$$
Lean4
/-- `CharP.quotient'` as an `Iff`. -/
theorem quotient_iff {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
CharP (R ⧸ I) n ↔ ∀ x : ℕ, ↑x ∈ I → (x : R) = 0 :=
by
refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩
rw [CharP.cast_eq_zero_iff R n, ← CharP.cast_eq_zero_iff (R ⧸ I) n _]
exact (Submodule.Quotient.mk_eq_zero I).mpr hx
