mul_apply — Mathlib

English

For additive automorphisms e1, e2 and a in A, their product acts by (e1 * e2)(a) = e1(e2(a)).

Русский

Для аддитивных автоморфизмов e1, e2 и элемента a в A произведение действует как (e1 * e2)(a) = e1(e2(a)).

LaTeX

$$$\forall e_1,e_2 \in \mathrm{AddAut}(A), \forall a \in A,\; (e_1 \cdot e_2)(a) = e_1(e_2(a))$$$

Lean4

@[simp]
theorem mul_apply (e₁ e₂ : AddAut A) (a : A) : (e₁ * e₂) a = e₁ (e₂ a) :=
  rfl

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