toLinearMapMonoidHom — Mathlib

English

For End_R(M), an endomorphism f is a unit if and only if it is bijective as a function.

Русский

Для End_R(M) эндоморфизм f является единицей тогда и только тогда, когда он биективен как отображение.

LaTeX

$$$ \text{IsUnit}(f) \iff \text{Bijective}(f) $$$

Lean4

/-- Restriction from `R`-linear automorphisms of `M` to `R`-linear endomorphisms of `M`,
promoted to a monoid hom. -/
@[simps]
def toLinearMapMonoidHom : (M ≃ₗ[R] M) →* M →ₗ[R] M
    where
  toFun e := e.toLinearMap
  map_one' := rfl
  map_mul' _ _ := rfl

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