con_ker_eq_conKer — Mathlib

English

The congruence defined by the kernel of a homomorphism equals the kernel as a congruence relation.

Русский

Конгруэнтность ядра гомоморфизма равна ядру как конгруэнтности.

LaTeX

$$QuotientGroup.con f.ker = Con.ker f$$

Lean4

/-- The congruence relation defined by the kernel of a group homomorphism is equal to its kernel
as a congruence relation.
-/
@[to_additive QuotientAddGroup.con_ker_eq_addConKer /--
    The additive congruence relation defined by the kernel of an additive group homomorphism is
    equal to its kernel as an additive congruence relation. -/
    ]
theorem con_ker_eq_conKer (f : G →* M) : QuotientGroup.con f.ker = Con.ker f :=
  by
  ext
  rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]

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