ModuleFinitePresentation

📁 Source: Mathlib/RingTheory/Finiteness/ModuleFinitePresentation.lean

Statistics

Metric	Count
Definitions	0
Theorems of_finitePresentation, exists_free_surjective, iff_finitePresentation_of_finite, of_finite_of_finitePresentation	4
Total	4

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finitePresentation 📖	mathematical	—	Algebra.FinitePresentation CommRing.toCommSemiring CommSemiring.toSemiring	—	Module.Finite.exists_free_surjective instFiniteOfFinitePresentation of_surjective Submodule.FG.of_restrictScalars RingHom.instRingHomClass IsScalarTower.right Module.FinitePresentation.fg_ker

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_free_surjective 📖	mathematical	—	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	Module.finite_def Finset.induction self Module.Free.self Algebra.FinitePresentation.self Finset.coe_empty Algebra.IsIntegral.isIntegral Algebra.IsIntegral.of_finite Polynomial.Monic.finite_adjoinRoot Polynomial.Monic.map minpoly.monic Polynomial.Monic.free_adjoinRoot trans AdjoinRoot.instIsScalarTower IsScalarTower.right Module.Free.trans Algebra.FinitePresentation.trans AdjoinRoot.finitePresentation IsScalarTower.of_algHom AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_map_algebraMap minpoly.aeval Finset.coe_insert AdjoinRoot.liftAlgHom_root HasSubset.Subset.trans Set.instIsTransSubset AdjoinRoot.liftAlgHom_of RingHomSurjective.ids Submodule.span_le LinearMap.range_eq_top top_le_iff

Module.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_finitePresentation_of_finite 📖	mathematical	—	Module.FinitePresentation CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.FinitePresentation	—	Algebra.FinitePresentation.of_finitePresentation of_finite_of_finitePresentation
of_finite_of_finitePresentation 📖	mathematical	—	Module.FinitePresentation CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	Module.Finite.exists_free_surjective IsScalarTower.of_algebraMap_eq' AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap Module.finitePresentation_of_projective Module.Projective.of_free Module.finitePresentation_of_surjective instFinitePresentation Algebra.FinitePresentation.ker_fG_of_surjective trans

---

← Back to Index