Documentation Verification Report

Localization

📁 Source: Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

Statistics

Metric	Count
Definitions	0
Theorems `comap_minimalPrimes_eq_of_surjective`, `disjoint_nonZeroDivisors_of_mem_minimalPrimes`, `exists_comap_eq_of_mem_minimalPrimes`, `exists_comap_eq_of_mem_minimalPrimes_of_injective`, `exists_minimalPrimes_comap_eq`, `exists_mul_mem_of_mem_minimalPrimes`, `iUnion_minimalPrimes`, `minimalPrimes_comap_subset`, `minimalPrimes_eq_comap`, `minimalPrimes_map_of_surjective`, `minimal_primes_comap_of_surjective`, `radical_map_of_mem_minimalPrimes`, `minimalPrimes_comap`, `minimalPrimes_map`, `notMem_of_mem_minimalPrimes`	15
Total	15

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_minimalPrimes_eq_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`minimalPrimes` `CommRing.toCommSemiring` `comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `Set.image` `Ideal`	—	`Set.ext` `RingHom.instRingHomClass` `exists_minimalPrimes_comap_eq` `minimal_primes_comap_of_surjective`
`disjoint_nonZeroDivisors_of_mem_minimalPrimes` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors`	—	`exists_mul_mem_of_mem_minimalPrimes`
`exists_comap_eq_of_mem_minimalPrimes` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`Ideal` `CommSemiring.toSemiring` `IsPrime` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `comap` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `exists_ideal_comap_le_prime` `LE.le.antisymm` `IsPrime.comap` `comap_mono`
`exists_comap_eq_of_mem_minimalPrimes_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Ideal` `Set` `Set.instMembership` `minimalPrimes`	`Ideal` `CommSemiring.toSemiring` `IsPrime` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `exists_comap_eq_of_mem_minimalPrimes` `comap_bot_of_injective`
`exists_minimalPrimes_comap_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `exists_comap_eq_of_mem_minimalPrimes` `exists_minimalPrimes_le` `LE.le.trans_eq` `comap_mono` `LE.le.antisymm` `IsPrime.comap`
`exists_mul_mem_of_mem_minimalPrimes` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Eq.subset` `Set.instReflSubset` `iUnion_minimalPrimes` `Set.mem_biUnion` `mul_pow` `pow_zero` `one_mul` `Nat.find_spec` `Nat.find_min` `mul_assoc` `pow_succ'` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub`
`iUnion_minimalPrimes` 📖	mathematical	—	`Set.iUnion` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `SetLike.coe` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `SetLike.instMembership` `radical` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Set.ext` `radical_eq_sInf` `le_sInf_iff` `Localization.isLocalization` `RingHom.instRingHomClass` `map_le_iff_le_comap` `mem_map_of_mem` `IsLocalization.mem_map_algebraMap_iff` `IsLocalization.eq_iff_exists` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsPrime.radical_le_iff` `mul_assoc` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `mul_mem_left` `IsPrime.mem_or_mem`
`minimalPrimes_comap_subset` 📖	mathematical	—	`Set` `Ideal` `CommSemiring.toSemiring` `Set.instHasSubset` `minimalPrimes` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `Set.image`	—	`RingHom.instRingHomClass` `exists_minimalPrimes_comap_eq`
`minimalPrimes_eq_comap` 📖	mathematical	—	`minimalPrimes` `CommRing.toCommSemiring` `Set.image` `Ideal` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Quotient.semiring` `CommSemiring.toSemiring` `comap` `RingHom` `Semiring.toNonAssocSemiring` `Quotient.ring` `instIsTwoSided_1` `RingHom.instFunLike` `RingHom.instRingHomClass` `minimalPrimes` `instHasQuotient_1` `Quotient.commSemiring`	—	`instIsTwoSided_1` `RingHom.instRingHomClass` `minimalPrimes.eq_1` `comap_minimalPrimes_eq_of_surjective` `Quotient.mk_surjective` `RingHom.ker_eq_comap_bot` `mk_ker`
`minimalPrimes_map_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`minimalPrimes` `CommRing.toCommSemiring` `map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `Set.image` `Ideal` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `Set.image_injective` `comap_injective_of_surjective` `comap_minimalPrimes_eq_of_surjective` `Set.image_comp` `comap_map_of_surjective` `Set.image_congr` `sup_eq_left` `LE.le.trans` `le_sup_right` `Set.image_id` `RingHom.ker.eq_1`
`minimal_primes_comap_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal` `Set` `Set.instMembership` `minimalPrimes`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `minimalPrimes` `comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `IsPrime.comap` `comap_mono` `LE.le.trans` `bot_le` `sup_eq_left` `RingHom.ker_eq_comap_bot` `comap_map_of_surjective` `map_isPrime_of_surjective` `le_map_of_comap_le_of_surjective` `map_le_of_le_comap`

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minimalPrimes_comap` 📖	mathematical	—	`Ideal.minimalPrimes` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Set.image` `Ideal`	—	`RingHom.instRingHomClass` `map_comap` `minimalPrimes_map` `Set.image_preimage_eq_iff` `subset_trans` `Set.instIsTransSubset` `Ideal.minimalPrimes_comap_subset` `Set.preimage_range`
`minimalPrimes_map` 📖	mathematical	—	`Ideal.minimalPrimes` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Set.preimage` `Ideal` `Ideal.comap` `RingHom.instRingHomClass`	—	`Set.ext` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `Ideal.map_le_iff_le_comap` `Set.disjoint_of_subset_right` `isPrime_iff_isPrime_disjoint` `LE.le.trans_eq` `Ideal.comap_mono` `isPrime_of_isPrime_disjoint` `Ideal.map_mono` `comap_map_of_isPrime_disjoint` `disjoint_comap_iff` `Ideal.IsPrime.ne_top` `map_comap`

IsLocalization.AtPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`radical_map_of_mem_minimalPrimes` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Ideal.minimalPrimes`	`Ideal.radical` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`isLocalRing` `Ideal.sInf_minimalPrimes` `RingHom.instRingHomClass` `IsLocalization.minimalPrimes_map` `le_antisymm` `sInf_le` `Set.mem_preimage` `map_eq_maximalIdeal` `comap_maximalIdeal` `le_sInf` `IsLocalization.comap_le_comap_iff` `Ideal.IsPrime.ne_top` `Set.disjoint_compl_left_iff_subset` `IsLocalization.disjoint_comap_iff` `Ideal.comap_eq_top_iff`

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`notMem_of_mem_minimalPrimes` 📖	mathematical	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Ideal` `Set` `Set.instMembership` `Ideal.minimalPrimes` `Module.annihilator`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.exists_mul_mem_of_mem_minimalPrimes` `Iff.not` `Module.mem_annihilator` `right_eq_zero_of_smul` `smul_smul`

---

← Back to Index