Documentation Verification Report

IsPrimary

📁 Source: Mathlib/RingTheory/IsPrimary.lean

Statistics

Metric	Count
Definitions `IsPrimary`	1
Theorems `inf`, `isPrime_radical_colon`, `mem_or_mem`, `ne_top`, `radical_colon_singleton_eq_ite`, `radical_colon_singleton_of_notMem`, `isPrimary_finsetInf`, `isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul`	8
Total	9

Submodule

Definitions

Name	Category	Theorems
`IsPrimary` 📖	MathDef	9 math math: `Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition`, `isPrimary_decomposition_pairwise_ne_radical`, `IsMinimalPrimaryDecomposition.primary`, `IsPrimary.inf`, `exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition`, `Ideal.isPrimary_decomposition_pairwise_ne_radical`, `isPrimary_finsetInf`, `isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul`, `InfIrred.isPrimary`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimary_finsetInf` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `IsPrimary` `Ideal.radical` `colon` `CommSemiring.toSemiring` `Set.univ`	`IsPrimary` `Finset.inf` `Submodule` `CommSemiring.toSemiring` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderTop`	—	`Finset.induction_on` `Finset.eq_empty_or_nonempty` `Finset.instLawfulSingleton` `Finset.inf_singleton` `Finset.inf_insert` `Finset.mem_insert_of_mem` `IsPrimary.inf` `colon_finsetInf` `Ideal.radical_finset_inf` `Finset.mem_insert_self`
`isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul` 📖	mathematical	—	`IsPrimary` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `HasQuotient.Quotient` `CommSemiring.toSemiring` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `pointwiseDistribMulAction` `Quotient.distribMulAction` `Quotient.smulCommClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Ring.toSemiring` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Monoid.toPow` `Top.top` `instTop` `Bot.bot` `instBot`	—	`Quotient.smulCommClass` `smulCommClass_self` `Function.Surjective.forall` `mkQ_surjective` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `ker_mkQ` `RingHomSurjective.ids` `LinearMap.range_eq_top` `map_top`

Submodule.IsPrimary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf` 📖	mathematical	`Submodule.IsPrimary` `Ideal.radical` `Submodule.colon` `CommSemiring.toSemiring` `Set.univ`	`Submodule.IsPrimary` `Submodule` `CommSemiring.toSemiring` `Submodule.instMin`	—	`smulCommClass_self` `Submodule.inf_colon` `Ideal.radical_inf` `inf_idem`
`isPrime_radical_colon` 📖	mathematical	`Submodule.IsPrimary`	`Ideal.IsPrime` `CommSemiring.toSemiring` `Ideal.radical` `Submodule.colon` `Set.univ`	—	`Ideal.isPrime_iff` `smulCommClass_self` `mul_pow` `SemigroupAction.mul_smul` `Ideal.mem_radical_of_pow_mem`
`mem_or_mem` 📖	mathematical	`Submodule.IsPrimary` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Ideal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.radical` `Submodule.colon` `Set.univ`	—	—
`ne_top` 📖	—	`Submodule.IsPrimary`	—	—	—
`radical_colon_singleton_eq_ite` 📖	mathematical	`Submodule.IsPrimary`	`Ideal.radical` `Submodule.colon` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Ideal` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set.univ`	—	`Ideal.radical_eq_top` `Submodule.colon_eq_top_iff_subset` `Set.singleton_subset_iff` `radical_colon_singleton_of_notMem`
`radical_colon_singleton_of_notMem` 📖	mathematical	`Submodule.IsPrimary` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike`	`Ideal.radical` `Submodule.colon` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Set.univ`	—	`le_antisymm` `Ideal.radical_le_radical_iff` `Submodule.mem_colon_singleton` `Ideal.radical_mono` `Submodule.colon_mono` `le_rfl` `Set.subset_univ`

---

← Back to Index