Documentation Verification Report

OrderOfVanishing

📁 Source: Mathlib/RingTheory/OrderOfVanishing.lean

Statistics

Metric	Count
Definitions `mulQuot`, `quotOfMul`, `ord`, `ordFrac`, `ordMonoidWithZeroHom`	5
Theorems `exact_mulQuot_quotOfMul`, `mulQuot_injective`, `quotOfMul_surjective`, `ordFrac_eq_div`, `ordFrac_eq_ord`, `ord_mul`, `ord_one`, `isFiniteLength_quotient_span_singleton`	8
Total	13

Ideal

Definitions

Name	Category	Theorems
`mulQuot` 📖	CompOp	2 math math: `exact_mulQuot_quotOfMul`, `mulQuot_injective`
`quotOfMul` 📖	CompOp	2 math math: `exact_mulQuot_quotOfMul`, `quotOfMul_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_mulQuot_quotOfMul` 📖	mathematical	—	`Function.Exact` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `span` `Set` `Set.instSingletonSet` `DFunLike.coe` `LinearMap` `RingHom.id` `Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `LinearMap.instFunLike` `mulQuot` `quotOfMul` `Submodule.Quotient.instZeroQuotient`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `Submodule.Quotient.smulCommClass` `instIsTwoSided_1` `Submodule.ker_liftQ` `Submodule.map.congr_simp` `Submodule.ker_mkQ` `Submodule.map_span` `Set.image_congr` `Set.image_singleton` `Quotient.smul_top` `Submodule.range_liftQ` `LinearMap.range_comp` `smulCommClass_self` `range_mul` `Submodule.restrictScalars_self` `LinearMap.map_span`
`mulQuot_injective` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`HasQuotient.Quotient` `Ideal` `instHasQuotient_1` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Submodule.pointwiseDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `DFunLike.coe` `LinearMap` `RingHom.id` `Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `LinearMap.instFunLike` `mulQuot`	—	`Algebra.to_smulCommClass` `Submodule.ker_liftQ_eq_bot'` `le_antisymm` `RingHomSurjective.ids` `smulCommClass_self` `IsScalarTower.right` `LinearMap.le_ker_iff_map` `Submodule.map_comp` `Submodule.mkQ_map_self` `ext` `IsScalarTower.to_smulCommClass'` `Submodule.mul_mem_smul_iff` `Submodule.ker_mkQ`
`quotOfMul_surjective` 📖	mathematical	—	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `Semiring.toModule` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submodule.pointwiseDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `span` `Set` `Set.instSingletonSet` `DFunLike.coe` `LinearMap` `RingHom.id` `Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `LinearMap.instFunLike` `quotOfMul`	—	`Algebra.to_smulCommClass` `Submodule.factor_surjective` `Submodule.smul_le_span` `Submodule.singleton_set_smul`

Ring

Definitions

Name	Category	Theorems
`ord` 📖	CompOp	2 math math: `ord_mul`, `ord_one`
`ordFrac` 📖	CompOp	2 math math: `ordFrac_eq_div`, `ordFrac_eq_ord`
`ordMonoidWithZeroHom` 📖	CompOp	2 math math: `ordFrac_eq_div`, `ordFrac_eq_ord`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ordFrac_eq_div` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `MonoidWithZeroHom.funLike` `ordFrac` `IsLocalization.mk'` `CommRing.toCommSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `WithZero.div` `Multiplicative.div` `ordMonoidWithZeroHom`	—	`IsFractionRing.mk'_eq_div` `map_div₀` `MonoidWithZeroHom.monoidWithZeroHomClass` `ordFrac_eq_ord`
`ordFrac_eq_ord` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `MonoidWithZeroHom.funLike` `ordFrac` `RingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `ordMonoidWithZeroHom`	—	`Function.Injective.isDomain` `instIsDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `Submonoid.LocalizationMap.lift_eq` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors`
`ord_mul` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`ord` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ENat` `Distrib.toAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instCommSemiringENat`	—	`Algebra.to_smulCommClass` `Module.length_eq_add_of_exact` `Ideal.mulQuot_injective` `Ideal.quotOfMul_surjective` `Ideal.exact_mulQuot_quotOfMul` `Submodule.set_smul_span` `Set.singleton_smul_singleton` `Submodule.singleton_set_smul` `mul_comm`
`ord_one` 📖	mathematical	—	`ord` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `toAddGroupWithOne` `ENat` `instZeroENat`	—	`Module.length_eq_zero` `Ideal.span_singleton_one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFiniteLength_quotient_span_singleton` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsFiniteLength` `CommRing.toRing` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `Submodule.Quotient.addCommGroup` `Ring.toAddCommGroup` `Semiring.toModule` `Submodule.Quotient.module`	—	`isFiniteLength_iff_isNoetherian_isArtinian` `isArtinianRing_iff_krullDimLE_zero` `Ideal.Quotient.isNoetherianRing` `Ring.KrullDimLE.eq_1` `Order.krullDimLE_iff` `WithBot.add_le_add_iff_right'` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Iff.not` `WithBot.coe_eq_coe` `Nat.cast_zero` `zero_add` `LE.le.trans` `ringKrullDim_quotient_succ_le_of_nonZeroDivisor` `Order.KrullDimLE.krullDim_le` `isNoetherian_quotient` `isArtinian_of_surjective_algebraMap` `Ideal.instIsTwoSided_1` `IsScalarTower.right` `Ideal.Quotient.mk_surjective`

---

← Back to Index