Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean

Statistics

Metric	Count
Definitions `IsAssociatedPrime`, `associatedPrimes`	2
Theorems `mem_iff`, `annihilator_le`, `eq_radical`, `isPrime`, `map_of_injective`, `eq`, `isAssociatedPrime_iff`, `eq_empty_of_subsingleton`, `eq_singleton_of_isPrimary`, `nonempty`, `prod`, `subset_of_injective`, `subset_union_of_exact`, `biUnion_associatedPrimes_eq_compl_nonZeroDivisors`, `biUnion_associatedPrimes_eq_zero_divisors`, `exists_le_isAssociatedPrime_of_isNoetherianRing`, `isAssociatedPrime_iff_exists_injective_linearMap`, `not_isAssociatedPrime_of_subsingleton`	18
Total	20

AssociatePrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `associatedPrimes` `IsAssociatedPrime`	—	—

IsAssociatedPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`annihilator_le` 📖	mathematical	`IsAssociatedPrime`	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.annihilator` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.bot_colon'` `Submodule.annihilator_mono` `le_top`
`eq_radical` 📖	mathematical	`Ideal.IsPrimary` `CommRing.toCommSemiring` `IsAssociatedPrime` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `Ideal.instHasQuotient_1` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule`	`Ideal.radical`	—	`Ideal.IsPrime.ne_top'` `Submodule.colon_singleton_zero` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mkₐ_surjective` `Submodule.mem_colon_singleton` `Submodule.mem_bot` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `smul_eq_mul` `mul_comm` `Submodule.Quotient.mk_eq_zero` `le_antisymm` `Ideal.isPrimary_iff` `Iff.not` `Ideal.IsPrime.radical_le_iff` `Ideal.mul_mem_left`
`isPrime` 📖	mathematical	`IsAssociatedPrime`	`Ideal.IsPrime` `CommSemiring.toSemiring`	—	—
`map_of_injective` 📖	—	`IsAssociatedPrime` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`Ideal.ext` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAssociatedPrime_iff` 📖	mathematical	—	`IsAssociatedPrime`	—	`RingHomInvPair.ids` `IsAssociatedPrime.map_of_injective` `injective`

LinearEquiv.AssociatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`associatedPrimes`	—	`RingHomInvPair.ids` `le_antisymm` `associatedPrimes.subset_of_injective` `LinearEquiv.injective`

(root)

Definitions

Name	Category	Theorems
`IsAssociatedPrime` 📖	MathDef	5 math math: `exists_le_isAssociatedPrime_of_isNoetherianRing`, `LinearEquiv.isAssociatedPrime_iff`, `AssociatePrimes.mem_iff`, `isAssociatedPrime_iff_exists_injective_linearMap`, `not_isAssociatedPrime_of_subsingleton`
`associatedPrimes` 📖	CompOp	15 math math: `biUnion_associatedPrimes_eq_compl_regular`, `Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule`, `Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing`, `associatedPrimes.finite`, `biUnion_associatedPrimes_eq_zero_divisors`, `associatedPrimes.nonempty`, `associatedPrimes.subset_of_injective`, `associatedPrimes.eq_singleton_of_isPrimary`, `associatedPrimes.eq_empty_of_subsingleton`, `AssociatePrimes.mem_iff`, `associatedPrimes.prod`, `LinearEquiv.AssociatedPrimes.eq`, `Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes`, `biUnion_associatedPrimes_eq_compl_nonZeroDivisors`, `associatedPrimes.subset_union_of_exact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_associatedPrimes_eq_compl_nonZeroDivisors` 📖	mathematical	—	`Set.iUnion` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `associatedPrimes` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.coe` `Submodule.setLike` `Compl.compl` `Set.instCompl` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors`	—	`biUnion_associatedPrimes_eq_zero_divisors` `Set.ext`
`biUnion_associatedPrimes_eq_zero_divisors` 📖	mathematical	—	`Set.iUnion` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `associatedPrimes` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.iUnion₂_subset` `Ideal.IsPrime.ne_top` `exists_le_isAssociatedPrime_of_isNoetherianRing` `Set.mem_biUnion` `Submodule.mem_colon_singleton`
`exists_le_isAssociatedPrime_of_isNoetherianRing` 📖	mathematical	—	`IsAssociatedPrime` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.colon` `Bot.bot` `Submodule` `Submodule.instBot` `Set` `Set.instSingletonSet`	—	`set_has_maximal_iff_noetherian` `Eq.le` `Submodule.mem_colon_singleton` `Submodule.mem_bot` `SMulCommClass.smul_comm` `smulCommClass_self` `smul_zero` `LE.le.eq_of_not_lt` `LE.le.trans` `smul_smul`
`isAssociatedPrime_iff_exists_injective_linearMap` 📖	mathematical	—	`IsAssociatedPrime` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ideal.IsPrime` `CommSemiring.toSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `LinearMap.instFunLike`	—	`IsAssociatedPrime.eq_1` `Eq.le` `LinearMap.ker_eq_bot` `Submodule.ker_liftQ_eq_bot'` `RingHomCompTriple.ids` `Submodule.ker_mkQ` `LinearMap.ker_comp_of_ker_eq_bot` `LinearMap.ker_eq_bot_of_injective` `Algebra.algebraMap_eq_smul_one` `one_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`not_isAssociatedPrime_of_subsingleton` 📖	mathematical	—	`IsAssociatedPrime`	—	`Ideal.IsPrime.ne_top` `Set.instReflSubset`

associatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_empty_of_subsingleton` 📖	mathematical	—	`associatedPrimes` `Set` `Ideal` `CommSemiring.toSemiring` `Set.instEmptyCollection`	—	`Set.ext` `not_isAssociatedPrime_of_subsingleton`
`eq_singleton_of_isPrimary` 📖	mathematical	`Ideal.IsPrimary` `CommRing.toCommSemiring`	`associatedPrimes` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `Ideal.instHasQuotient_1` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Set` `Set.instSingletonSet` `Ideal.radical`	—	`Set.ext` `Set.mem_singleton_iff` `IsAssociatedPrime.eq_radical` `nonempty` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq` `sub_zero` `Ideal.eq_top_iff_one`
`nonempty` 📖	mathematical	—	`Set.Nonempty` `Ideal` `CommSemiring.toSemiring` `associatedPrimes`	—	`exists_ne` `exists_le_isAssociatedPrime_of_isNoetherianRing`
`prod` 📖	mathematical	—	`associatedPrimes` `Prod.instAddCommMonoid` `Prod.instModule` `CommSemiring.toSemiring` `Set` `Ideal` `Set.instUnion`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `subset_union_of_exact` `LinearMap.inl_injective` `Function.Exact.inl_snd` `Set.union_subset_iff` `subset_of_injective` `LinearMap.inr_injective`
`subset_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Set` `Ideal` `Set.instHasSubset` `associatedPrimes`	—	`IsAssociatedPrime.map_of_injective`
`subset_union_of_exact` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Function.Exact` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Set` `Ideal` `Set.instHasSubset` `associatedPrimes` `Set.instUnion`	—	`le_antisymm` `Submodule.mem_colon_singleton` `Submodule.mem_bot` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SMulCommClass.smul_comm` `smulCommClass_self` `smul_zero` `Mathlib.Tactic.Contrapose.contrapose₁` `Submonoid.mul_mem` `SemigroupAction.mul_smul` `RingHomSurjective.ids` `Function.Exact.linearMap_ker_eq` `LinearMap.mem_ker` `Mathlib.Tactic.Push.not_and_eq`

---

← Back to Index