coe_mul

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#MulAut.coe_mul

English

The product of two multiplicative automorphisms corresponds to their functional composition.

Русский

Произведение двух мультипликативных автоматов соответствует композиции функций.

LaTeX

$$$$ (e_{1} \\cdot e_{2})(x) = e_{1}(e_{2}(x)) \\quad \\text{for all } x \\in M. $$$$

Lean4

@[simp]
theorem coe_mul (e₁ e₂ : MulAut M) : ⇑(e₁ * e₂) = e₁ ∘ e₂ :=
  rfl

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

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

Разделы

Аффилиация

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