coe_toMultiplicative_ker — Mathlib

English

The kernel of the AddMonoidHom toMultiplicative version matches the AddSubgroup of the original ker.

Русский

Ядро отображения AddMonoidHom в toMultiplicative соответствует AddSubgroup предыдущего ядра.

LaTeX

$$$\ker(\mathrm{toMultiplicative}(f)) = \mathrm{AddSubgroup}(\ker f)$$$

Lean4

@[simp]
theorem coe_toMultiplicative_ker {A A' : Type*} [AddGroup A] [AddZeroClass A'] (f : A →+ A') :
    (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker :=
  rfl

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