toSubmonoid_inj

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.toSubmonoid_inj

English

For subgroups p and q, p.toSubmonoid = q.toSubmonoid iff p = q.

Русский

Для подгрупп p и q верно: p.toSubmonoid = q.toSubmonoid тогда и только тогда p = q.

LaTeX

$$$p.toSubmonoid = q.toSubmonoid \\iff p = q$$$

Lean4

@[to_additive (attr := simp)]
theorem toSubmonoid_inj {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q :=
  toSubmonoid_injective.eq_iff

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

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

Разделы

Аффилиация

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