applyDistribMulAction — Mathlib

English

The collection of all R-linear automorphisms of M forms a group under composition.

Русский

Множество всех R-линейных автоморфизмов M образует группу под операцией композиции.

LaTeX

$$$ \mathrm{Aut}_R(M) \text{ is a group under composition. } $$$

Lean4

/-- The tautological action by `M ≃ₗ[R] M` on `M`.

This generalizes `Function.End.applyMulAction`. -/
instance applyDistribMulAction : DistribMulAction (M ≃ₗ[R] M) M
    where
  smul := (· <| ·)
  smul_zero := LinearEquiv.map_zero
  smul_add := LinearEquiv.map_add
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

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