Documentation Verification Report

HasFiniteQuotients

📁 Source: Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean

Statistics

Metric	Count
Definitions `HasFiniteQuotients`	1
Theorems `cardQuot_pos`, `finiteQuotient`, `finite_absNorm_heightOneSpectrum_le`, `finite_absNorm_le`, `finite_cardQuot_heightOneSpectrum_le`, `finite_cardQuot_le`, `finite_setOf_mem`, `instDimensionLEOne`, `instInt`, `instIsNoetherianRing`, `instOfFinite`, `instOfIsDomainOfFG`, `maximalOfPrime`, `of_module_finite`	14
Total	15

Ring

Definitions

Name	Category	Theorems
`HasFiniteQuotients` 📖	CompData	4 math math: `HasFiniteQuotients.instOfIsDomainOfFG`, `HasFiniteQuotients.instInt`, `HasFiniteQuotients.of_module_finite`, `HasFiniteQuotients.instOfFinite`

Ring.HasFiniteQuotients

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardQuot_pos` 📖	mathematical	—	`Submodule.cardQuot` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`finiteQuotient` `Submodule.cardQuot_apply` `Nat.card_pos` `Ideal.Quotient.instNonemptyQuotient` `Ideal.instIsTwoSided_1`
`finiteQuotient` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1`	—	—
`finite_absNorm_heightOneSpectrum_le` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `setOf` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`finite_cardQuot_heightOneSpectrum_le`
`finite_absNorm_le` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain`	—	`finite_cardQuot_le`
`finite_cardQuot_heightOneSpectrum_le` 📖	mathematical	—	`Set.Finite` `IsDedekindDomain.HeightOneSpectrum` `setOf` `Submodule.cardQuot` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`Set.Finite.of_injOn` `Function.Injective.injOn` `IsDedekindDomain.HeightOneSpectrum.ext` `finite_cardQuot_le`
`finite_cardQuot_le` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `Submodule.cardQuot` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule`	—	`finite_or_infinite` `Set.toFinite` `Subtype.finite` `SetLike.instFinite` `Infinite.exists_subset_card_eq` `Set.Finite.of_diff` `Ideal.instIsTwoSided_1` `finiteQuotient` `Submodule.cardQuot_apply` `Set.mem_setOf` `Set.mem_diff` `lt_imp_lt_of_le_of_le` `Finset.card_le_univ` `le_refl` `Fintype.card_eq_nat_card` `Finset.exists_ne_map_eq_of_card_image_lt` `Finset.mem_sdiff` `Finset.mem_sub` `Finset.notMem_singleton` `sub_ne_zero` `Submodule.Quotient.eq` `Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `finite_setOf_mem` `Set.finite_singleton`
`finite_setOf_mem` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`finiteQuotient` `Ideal.span_singleton_eq_bot` `Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `Finite.of_equiv` `SetLike.instFinite` `Ideal.Quotient.mk_surjective` `Ideal.mk_ker`
`instDimensionLEOne` 📖	mathematical	—	`Ring.DimensionLEOne`	—	`maximalOfPrime`
`instInt` 📖	mathematical	—	`Ring.HasFiniteQuotients` `Int.instCommRing`	—	`Submodule.IsPrincipal.principal` `IsPrincipalIdealRing.principal` `EuclideanDomain.to_principal_ideal_domain`
`instIsNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`isNoetherianRing_iff_ideal_fg` `Submodule.fg_bot` `Submodule.exists_mem_ne_zero_of_ne_bot` `Submodule.fg_of_fg_map_of_fg_inf_ker` `finiteQuotient` `Submodule.FG.of_finite` `RingHomSurjective.ids` `Module.IsNoetherian.finite` `isNoetherian_submodule'` `isNoetherian_of_finite` `Submodule.ker_mkQ` `inf_eq_right` `Ideal.span_singleton_le_iff_mem` `Submodule.fg_span_singleton`
`instOfFinite` 📖	mathematical	—	`Ring.HasFiniteQuotients`	—	`Quotient.finite`
`instOfIsDomainOfFG` 📖	mathematical	—	`Ring.HasFiniteQuotients`	—	`of_module_finite` `instInt` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg`
`maximalOfPrime` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`finiteQuotient` `Ideal.Quotient.maximal_of_isField` `Finite.isField_of_domain` `Ideal.Quotient.isDomain` `Ideal.instIsTwoSided_1`
`of_module_finite` 📖	mathematical	—	`Ring.HasFiniteQuotients`	—	`subsingleton_or_nontrivial` `Module.finite_of_finite` `Finite.of_subsingleton` `Quotient.finite` `finiteQuotient` `Ideal.under_ne_bot` `Algebra.IsIntegral.of_finite` `Module.Finite.of_restrictScalars_finite` `IsScalarTower.right` `Ideal.Quotient.isScalarTower_of_liesOver` `IsScalarTower.left` `Ideal.over_under` `Module.Finite.quotient`

---

← Back to Index