apply_smulCommClass' — Mathlib

English

Restriction from linear automorphisms to linear endomorphisms defines a monoid homomorphism.

Русский

Ограничение линейных автоморфизмов на линейные эндоморфизмы задаёт гомоморфизм моноида.

LaTeX

$$$ \mathrm{toLinearMapMonoidHom } : (M \simeq_R M) \to* M \to_{R} M $$$

Lean4

instance apply_smulCommClass' [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (M ≃ₗ[R] M) S M :=
  SMulCommClass.symm _ _ _

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