mul_eq

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.IsComplement.mul_eq

English

If H and K are complements, then the product S·T equals the whole group, i.e., S·T = G.

Русский

Если H и K — дополнения, то произведение S·T охватывает всю группу: S·T = G.

LaTeX

$$$ \text{IsComplement } S T \Rightarrow S \cdot T = \mathrm{univ}. $$$

Lean4

@[to_additive]
theorem mul_eq (h : IsComplement S T) : S * T = univ :=
  eq_univ_of_forall fun x ↦ by simpa [mem_mul] using (h.existsUnique x).exists

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

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

Разделы

Аффилиация

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