coe_mul — Mathlib

English

For all AddAut(A) elements e1 and e2, the product e1 * e2 acts as function composition: the underlying function of e1 * e2 is e1 ∘ e2, i.e., (e1 * e2)(x) = e1(e2(x)) for all x.

Русский

Для любых e1, e2 ∈ AddAut(A) произведение e1 * e2 действует как композиция функций: (e1 * e2)(x) = e1(e2(x)) для всех x.

LaTeX

$$$ (e_1 * e_2)(x) = e_1(e_2(x)) \quad \text{for all } x \in A $$$

Lean4

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

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