div_mem_ker_iff

Mathlib.Algebra.Group.Subgroup.Ker

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

English

For a group hom f, x y^{-1} lies in the kernel iff f(x) = f(y).

Русский

Для гомоморфизма f верно: x y^{-1} ∈ ker f тогда и только тогда, когда f(x) = f(y).

LaTeX

$$$$ x y^{-1} \\in \\ker f \\iff f(x) = f(y) $$$$

Lean4

@[to_additive]
theorem div_mem_ker_iff (f : G →* N) {x y : G} : x / y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_div, div_eq_one]

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

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

Разделы

Аффилиация

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