End — Mathlib

English

End_R(M) denotes the set of all R-linear maps from M to itself; i.e., End_R(M) = Hom_R(M,M).

Русский

End_R(M) обозначает множество всех R-линейных отображений из M в себя; тождественно End_R(M) = Hom_R(M,M).

LaTeX

$$\mathrm{End}_R(M) = \{ f: M \to M \mid f \text{ is } R\text{-linear} \}$$

Lean4

/-- Linear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`. -/
abbrev End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :=
  M →ₗ[R] M

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