coe_toAdditive_ker — Mathlib

English

The kernel commutes with the passage from multiplicative to additive structure: the additive kernel corresponds to the additive kernel of f.

Русский

Ядро сохраняется при переходе от мультипликативной структуры к аддитивной: аддитивное ядро соответствует аддитивному ядру f.

LaTeX

$$$\ker(\mathrm{to\,Additive}(f)) = \mathrm{toAddSubgroup}(\ker f)$$$

Lean4

@[simp]
theorem coe_toAdditive_ker (f : G →* G') : (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker :=
  rfl

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