Finite

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_ext` 📖	mathematical	—	`Module.Finite` `CategoryTheory.Abelian.Ext` `ModuleCat` `CommRing.toRing` `moduleCategory` `abelian` `instHasExtModuleCatOfSmall` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Abelian.Ext.instAddCommGroup` `CategoryTheory.Abelian.Ext.instModule` `instLinear`	—	`instHasExtModuleCatOfSmall` `Module.Finite.equiv` `Algebra.instSMulCommClassCarrier` `Module.IsNoetherian.finite` `isNoetherian_linearMap` `isNoetherian_of_isNoetherianRing_of_finite` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Module.exists_finite_presentation` `LinearMap.shortExact_shortComplexKer` `Module.Finite.of_surjective` `RingHomSurjective.ids` `isNoetherian_submodule'` `add_comm` `precomp_extClass_surjective_of_projective_X₂` `projective_of_categoryTheory_projective` `Module.Projective.of_free`

---