ker_snd

Mathlib.Algebra.Group.Subgroup.Basic

URI: https://scilib.ai/kg/mathlib#MonoidHom.ker_snd

English

The kernel of the second projection is the first factor.

Русский

Ядро проекции на вторую координату равно первой фактор.

LaTeX

$$$ \\ker (\\\\mathrm{snd}) = G \\\\times \\\\{e_{G'}\\\\} $$$

Lean4

@[to_additive (attr := simp)]
theorem ker_snd : ker (snd G G') = .prod ⊤ ⊥ :=
  SetLike.ext fun _ => (iff_of_eq (true_and _)).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru