ker_intCastAddHom — Mathlib

English

The kernel of the additive map Int.castAddHom(ZMod n) equals the subgroup of integer multiples of n.

Русский

Ядро отображения Int.castAddHom(ZMod n) равно подгруппе целочисленных кратных n.

LaTeX

$$$\mathrm{ker}\big(\operatorname{Int.castAddHom}(\mathbb{Z}/n\mathbb{Z})\big) = \mathbb{Z}\cdot n$$$

Lean4

theorem ker_intCastAddHom (n : ℕ) : (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples (n : ℤ) :=
  by
  ext
  rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom, intCast_zmod_eq_zero_iff_dvd]

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