Theorems · Definition · category theory
ModuleCat.isFG
(R : Type u) → [inst : Ring R] → CategoryTheory.ObjectProperty (ModuleCat R)
Finitely generated modules, as a property of objects of ModuleCat R.
- Cited by
- 53 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- ModuleCatstatement and proof · cited by 1,429
- Module.Finiteproof · cited by 1,032
- ModuleCat.carrierproof · cited by 997
- CategoryTheory.ObjectPropertystatement · cited by 798
Cited by79
Results whose statement or proof uses this declaration.
- FGModuleCatproof · cited by 52
- FDRep.ρstatement · cited by 20
- TannakaDuality.FiniteGroup.forgetstatement · cited by 9
- TannakaDuality.FiniteGroup.equivAppstatement · cited by 4
- FGModuleCat.isoToLinearEquivstatement · cited by 3
- TannakaDuality.FiniteGroup.equivHomstatement · cited by 3
- TannakaDuality.FiniteGroup.sumSMulInvstatement · cited by 3
- FDRep.isoToLinearEquivstatement · cited by 2
- FDRep.scalar_product_char_eq_finrank_equivariantstatement · cited by 2
- FGModuleCat.FGModuleCatEvaluationstatement · cited by 2
- FGModuleCat.hom_extstatement and proof · cited by 2
- TannakaDuality.FiniteGroup.algHomOfRightFDRepCompstatement · cited by 2