mem_graph

Mathlib.Algebra.Group.Graph

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

English

The graph of a group homomorphism f : G →* H is a subgroup of G × H.

Русский

Граф гомоморфизма групп f : G →* H является подгруппой G × H.

LaTeX

$$$f.graph \\leq G \\times H$ as a Subgroup of $G \\times H$ with $\\text{toSubmonoid}(f.graph) = f.mgraph$.$$

Lean4

@[to_additive]
theorem mem_graph {f : G →* H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2 :=
  .rfl

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

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

Разделы

Аффилиация

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