Quotient

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

Statistics

Metric	Count
Definitions	0
Theorems isNoetherian, algebra_finiteType_of_liesOver, isNoetherian_of_liesOver, module_finite_of_liesOver	4
Total	4

QuotientMapQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNoetherian 📖	mathematical	—	IsNoetherian HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Ideal.Quotient.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Ideal.Quotient.commSemiring Ideal.Quotient.algebraQuotientMapQuotient	—	isNoetherian_of_tower Ideal.instIsTwoSided_1 Ideal.Quotient.tower_quotient_map_quotient isNoetherian_of_surjective RingHomSurjective.ids LinearMap.range_eq_top Ideal.Quotient.mk_surjective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebra_finiteType_of_liesOver 📖	mathematical	—	Algebra.FiniteType HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring Ideal.Quotient.semiring Ideal.Quotient.algebraOfLiesOver	—	Algebra.FiniteType.of_restrictScalars_finiteType Ideal.Quotient.isScalarTower_of_liesOver IsScalarTower.left Algebra.FiniteType.quotient
isNoetherian_of_liesOver 📖	mathematical	—	IsNoetherian HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Ideal.Quotient.commSemiring Ideal.Quotient.algebraOfLiesOver	—	isNoetherian_of_tower IsScalarTower.right Ideal.Quotient.isScalarTower_of_liesOver IsScalarTower.left isNoetherian_quotient
module_finite_of_liesOver 📖	mathematical	—	Module.Finite HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Ideal.Quotient.commSemiring Ideal.Quotient.algebraOfLiesOver	—	Module.Finite.of_restrictScalars_finite IsScalarTower.right Ideal.Quotient.isScalarTower_of_liesOver IsScalarTower.left Module.Finite.quotient

---

← Back to Index