mul_apply — Mathlib

English

Let e1 and e2 be multiplicative automorphisms of M and m ∈ M. The action of their product on m is the sequential action: (e1 e2)(m) = e1(e2(m)).

Русский

Пусть e1 и e2 — автоморфизмы умножения M. Тогда (e1 e2)(m) = e1(e2(m)) для любого m ∈ M.

LaTeX

$$$ \forall e_1,e_2 \in \mathrm{MulAut}(M), \forall m \in M,\; (e_1 \cdot e_2)(m) = e_1(e_2(m)) $$$

Lean4

@[simp]
theorem mul_apply (e₁ e₂ : MulAut M) (m : M) : (e₁ * e₂) m = e₁ (e₂ m) :=
  rfl

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