mulLeft_mul

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.mulLeft_mul

English

Left translation by a b equals the product of left translations by a and by b.

Русский

Левая трансляция на a b равна произведению левых трансляций на a и на b.

LaTeX

$$$$ \\mathrm{mulLeft}(a b) = \\mathrm{mulLeft}(a) \\cdot \\mathrm{mulLeft}(b). $$$$

Lean4

@[simp]
theorem mulLeft_mul : Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b :=
  ext <| mul_assoc _ _

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

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

Разделы

Аффилиация

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