mulRight_mul

Mathlib.Algebra.Group.End

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

English

Right translation by ab equals the product of right translations by b and by a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mulRight_mul : Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a :=
  ext fun _ ↦ (mul_assoc _ _ _).symm

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

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

Разделы

Аффилиация

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