Documentation Verification Report

Quotient

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

Statistics

Metric	Count
Definitions `basisQuotient`	1
Theorems `basisQuotient_apply`, `basisQuotient_repr`, `exists_maximalIdeal_pow_le_of_finite_quotient`, `exists_maximalIdeal_pow_le_of_isArtinianRing_quotient`, `finite_quotient_iff`, `finrank_quotient_map`, `quotient_span_eq_top_iff_span_eq_top`	7
Total	8

IsLocalRing

Definitions

Name	Category	Theorems
`basisQuotient` 📖	CompOp	2 math math: `basisQuotient_repr`, `basisQuotient_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `maximalIdeal` `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` `Module.Basis.instFunLike` `basisQuotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1` `coe_basisOfTopLeSpanOfCardEqFinrank`
`basisQuotient_repr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `maximalIdeal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ideal.Quotient.semiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Ideal.Quotient.commSemiring` `Ideal.Quotient.algebraQuotientMapQuotient` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basisQuotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`RingHomInvPair.ids` `Ideal.instIsTwoSided_1` `LinearEquiv.injective` `Finite.of_fintype` `Finsupp.linearEquivFunOnFinite_symm_coe` `LinearEquiv.symm_apply_apply` `Module.Basis.repr_symm_apply` `Finsupp.linearCombination_eq_fintype_linearCombination_apply` `Fintype.linearCombination_apply` `Finset.sum_congr` `basisQuotient_apply` `Ideal.Quotient.mk_smul_mk_quotient_map_quotient` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Module.Basis.sum_repr`
`exists_maximalIdeal_pow_le_of_finite_quotient` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `maximalIdeal`	—	`exists_maximalIdeal_pow_le_of_isArtinianRing_quotient`
`exists_maximalIdeal_pow_le_of_isArtinianRing_quotient` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `maximalIdeal`	—	`Ideal.Quotient.nontrivial_iff` `of_surjective'` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `IsLocalHom.of_surjective` `IsScalarTower.left` `IsArtinianRing.isNilpotent_jacobson_bot` `Ideal.ext` `sup_eq_left` `le_maximalIdeal` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.right` `Ideal.mk_ker` `Ideal.map_eq_bot_iff_le_ker` `Ideal.zero_eq_bot` `Ideal.map_pow` `jacobson_eq_maximalIdeal` `bot_ne_top` `Ideal.instNontrivial`
`finite_quotient_iff` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `maximalIdeal`	—	`exists_maximalIdeal_pow_le_of_isArtinianRing_quotient` `isArtinian_of_fg_of_artinian'` `Finite.to_wellFoundedLT` `SetLike.instFinite` `Module.Finite.self` `Ideal.finite_quotient_pow` `IsNoetherian.noetherian` `Finite.of_surjective` `Ideal.instIsTwoSided_1` `Ideal.Quotient.factor_surjective`
`finrank_quotient_map` 📖	mathematical	—	`Module.finrank` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `maximalIdeal` `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`	—	`Module.Finite.of_restrictScalars_finite` `IsScalarTower.right` `Ideal.Quotient.tower_quotient_map_quotient` `Module.Finite.quotient` `le_antisymm` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `toNontrivial` `finrank_le_of_span_eq_top` `maximalIdeal.isMaximal` `Field.instIsLocalRing` `Ideal.instIsTwoSided_1` `Set.range_comp` `quotient_span_eq_top_iff_span_eq_top` `Module.Basis.span_eq` `Module.free_of_finite_type_torsion_free'` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Ideal.Quotient.isDomain` `Ideal.IsMaximal.isPrime'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Ideal.Quotient.mk_surjective`
`quotient_span_eq_top_iff_span_eq_top` 📖	mathematical	—	`Submodule.span` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `maximalIdeal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `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` `Set.image` `DFunLike.coe` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Top.top` `Submodule` `Submodule.instTop`	—	`IsScalarTower.right` `Ideal.Quotient.tower_quotient_map_quotient` `Ideal.instIsTwoSided_1` `RingHomSurjective.ids` `Ideal.Quotient.isScalarTower` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Submodule.map_span` `Submodule.restrictScalars_span` `Ideal.Quotient.mk_surjective` `LinearMap.coe_coe` `IsScalarTower.coe_toAlgHom'` `Ideal.Quotient.algebraMap_eq` `top_le_iff` `Submodule.le_of_le_smul_of_le_jacobson_bot` `Module.finite_def` `Eq.ge` `jacobson_eq_maximalIdeal` `bot_ne_top` `Ideal.instNontrivial` `toNontrivial` `IsScalarTower.left` `Ideal.smul_top_eq_map` `Submodule.ext` `Submodule.comap_map_eq` `Submodule.mem_comap` `Submodule.restrictScalars_top` `Submodule.mem_top` `Submodule.restrictScalars_eq_top_iff` `LinearMap.range_eq_top` `Submodule.map_top`

---

← Back to Index