applyMulAction — Mathlib

Lean4
/-- The tautological action by `Function.End α` on `α`.

This is generalized to bundled endomorphisms by:
* `Equiv.Perm.applyMulAction`
* `AddMonoid.End.applyDistribMulAction`
* `AddMonoid.End.applyModule`
* `AddAut.applyDistribMulAction`
* `MulAut.applyMulDistribMulAction`
* `LinearEquiv.applyDistribMulAction`
* `LinearMap.applyModule`
* `RingHom.applyMulSemiringAction`
* `RingAut.applyMulSemiringAction`
* `AlgEquiv.applyMulSemiringAction`
* `RelHom.applyMulAction`
* `RelEmbedding.applyMulAction`
* `RelIso.applyMulAction`
-/
instance applyMulAction : MulAction (Function.End α) α
    where
  smul := (· <| ·)
  one_smul _ := rfl
  mul_smul _ _ _ := rfl
Похожие утверждения