mul_comm_of_mem_isMulCommutative

Mathlib.Algebra.Group.Subgroup.Defs

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

← MathLib Explorer

English

If a,b ∈ H, then a b = b a.

Русский

Если a, b ∈ H, то a b = b a.

LaTeX

$$$a,b \\in H \\Rightarrow a b = b a$$$

Lean4

@[to_additive]
theorem mul_comm_of_mem_isMulCommutative [IsMulCommutative H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a * b = b * a := by
  simpa only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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