instMulActionOrderIso — Mathlib

English

The action of OrderIso on Flag α is a genuine multiplicative action: e1 • (e2 • s) = (e1 ∘ e2) • s and 1 • s = s.

Русский

Действие OrderIso на Flag α удовлетворяет свойствам мультикоэффициентного действия: e1 • (e2 • s) = (e1 ∘ e2) • s; 1 • s = s.

LaTeX

$$e1 \cdot (e2 \cdot s) = (e1 \circ e2) \cdot s, \quad 1 \cdot s = s$$

Lean4

instance : MulAction (α ≃o α) (Flag α) :=
  SetLike.coe_injective.mulAction _ coe_smul

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