Theorems · Definition · category theory

FGModuleCat.of

(R : Type u) →
  [inst : Ring R] →
    (V : Type v) → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [Module.Finite R V] → FGModuleCat R

Lift an unbundled finitely generated module to FGModuleCat R.

Defined in

Mathlib.Algebra.Category.FGModuleCat.Basic

Cited by

5 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleModule.Finite