toLinearEquiv — Mathlib

English

Every group element defines a module automorphism of M, yielding a monoid hom from the group to linear automorphisms of M.

Русский

Каждый элемент группы определяет модульный автоморфизм M, давая гомоморфизм моноида от группы к линейным автоморфизмам M.

LaTeX

$$$ toModuleAut : S \to* M \simeq_R M $$$

Lean4

/-- Each element of the group defines a linear equivalence.

This is a stronger version of `DistribMulAction.toAddEquiv`. -/
@[simps!]
def toLinearEquiv (s : S) : M ≃ₗ[R] M :=
  { toAddEquiv M s, toLinearMap R M s with }

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