Theorems · Definition · ring theory

Module.End

(R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type v

Linear endomorphisms of a module, with associated ring structure Module.End.semiring and algebra structure Module.End.algebra.

Defined in

Mathlib.Algebra.Module.LinearMap.End

Cited by

774 results in Mathlib

Foundations

Depth 13 from the axioms, rests on 111 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModule