Documentation Verification Report

IntegrallyClosed

📁 Source: Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean

Statistics

Metric	Count
Definitions	0
Theorems `iInf`, `of_iInf_eq_bot`, `of_isLocalization_maximal`, `of_localization`, `of_localization_maximal`, `of_localization_submonoid`, `isIntegrallyClosed_ofLocalizationMaximal`	7
Total	7

IsIntegrallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf` 📖	mathematical	`IsIntegrallyClosed` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`isIntegrallyClosed_iff` `Localization.subalgebra.instIsFractionRingSubtypeMemSubalgebra` `CanLift.prf` `Subtype.canLift` `Algebra.mem_iInf` `iInf_le` `Subalgebra.inclusion.isScalarTower_right` `IsIntegral.tower_top`
`of_iInf_eq_bot` 📖	—	`IsIntegrallyClosed` `Subalgebra` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—	`FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `of_equiv` `iInf`
`of_isLocalization_maximal` 📖	—	`IsLocalization.AtPrime` `CommRing.toCommSemiring` `Ideal.IsMaximal.isPrime'` `IsIntegrallyClosed`	—	—	`Ideal.IsMaximal.isPrime'` `of_localization_maximal` `of_equiv` `Localization.isLocalization` `Submonoid.map_id`
`of_localization` 📖	—	`IsIntegrallyClosed` `Localization.AtPrime` `CommRing.toCommSemiring` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `iInf` `Subalgebra` `FractionRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Algebra.id` `PrimeSpectrum` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Set` `Set.instMembership` `Localization.subalgebra` `Localization.isLocalization` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—	`PrimeSpectrum.isPrime` `Localization.isLocalization` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `of_localization_submonoid` `Subalgebra.ext`
`of_localization_maximal` 📖	—	`IsIntegrallyClosed` `Localization.AtPrime` `CommRing.toCommSemiring` `Ideal.IsMaximal.isPrime'` `OreLocalization.instCommRing` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid`	—	—	`Ideal.IsMaximal.isPrime'` `Field.instIsIntegrallyClosed` `of_localization` `PrimeSpectrum.isPrime` `Ring.ne_bot_of_isMaximal_of_not_isField` `IsDomain.toNontrivial` `MaximalSpectrum.isMaximal` `Localization.isLocalization` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `iInf_range` `Localization.subalgebra.ofField_eq` `MaximalSpectrum.toPrimeSpectrum.eq_1` `MaximalSpectrum.iInf_localization_eq_bot`
`of_localization_submonoid` 📖	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero` `IsIntegrallyClosed` `Localization` `CommRing.toCommMonoid` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `iInf` `Subalgebra` `FractionRing` `OreLocalization.instAlgebra` `Algebra.id` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Localization.subalgebra` `Localization.isLocalization` `Bot.bot` `OrderBot.toBot` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—	`Localization.isLocalization` `of_iInf_eq_bot` `of_equiv` `Localization.subalgebra.isLocalization_subalgebra`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegrallyClosed_ofLocalizationMaximal` 📖	mathematical	—	`OfLocalizationMaximal`	—	`IsIntegrallyClosed.of_localization_maximal` `IsLocalization.isDomain_of_local_atPrime`

---

← Back to Index