ker_intAlgebraMap_eq_span — Mathlib

English

The kernel of the natural map from the integers to a ring R equals the ideal generated by p when CharP(R,p).

Русский

Ядро отображения из целых в кольцо R равно идеалу, порождаемому p, если CharP(R,p).

LaTeX

$$$\\operatorname{ker}(\\text{algebraMap } \\mathbb{Z} \\to R) = \\operatorname{Ideal}.\\operatorname{span}\\{p\\}$$$

Lean4

theorem ker_intAlgebraMap_eq_span {R : Type*} [Ring R] (p : ℕ) [CharP R p] :
    RingHom.ker (algebraMap ℤ R) = Ideal.span {(p : ℤ)} :=
  by
  ext a
  simp [CharP.intCast_eq_zero_iff R p, Ideal.mem_span_singleton]

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