Theorems · Definition · category theory

SemimoduleCat.of

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

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of SemimoduleCat R.

Defined in

Mathlib.Algebra.Category.ModuleCat.Semi

Cited by

25 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidModule