applyMulAction — Mathlib

English

The tautological action of the permutation group on α is the standard action by evaluation: f • a = f(a).

Русский

Один к одному: тождественное действие группы перестановок на α — обычное действие по применению к элементу.

LaTeX

$$$ f \cdot a = f(a) $$$

Lean4

/-- The tautological action by `Equiv.Perm α` on `α`.

This generalizes `Function.End.applyMulAction`. -/
instance applyMulAction (α : Type*) : MulAction (Perm α) α
    where
  smul f a := f a
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

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