Documentation Verification Report

IntegrallyClosed

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

Statistics

Metric	Count
Definitions `IsIntegrallyClosedIn`	1
Theorems `isIntegrallyClosedIn`, `isIntegrallyClosedIn`, `pow_iff`, `instIsIntegrallyClosed`, `of_isIntegralClosure_of_isIntegrallyClosedIn`, `of_isIntegrallyClosed`, `of_isIntegrallyClosedIn`, `algebraMap_eq_of_integral`, `exists_algebraMap_eq_of_isIntegral_pow`, `exists_algebraMap_eq_of_pow_mem_subalgebra`, `instIsIntegralClosure`, `integralClosure_eq_bot`, `integralClosure_eq_bot_iff`, `isIntegral_iff`, `of_equiv`, `of_isIntegrallyClosedIn`, `of_isIntegrallyClosed_of_isIntegrallyClosedIn`, `pow_dvd_pow_iff`, `algebraMap_eq_of_integral`, `exists_algebraMap_eq_of_isIntegral_pow`, `exists_algebraMap_eq_of_pow_mem_subalgebra`, `inst`, `integralClosure_eq_bot`, `integralClosure_eq_bot_iff`, `isIntegral_iff`, `of_isIntegralClosure`, `integralClosure_le_iff`, `integralClosure_subring_le_iff`, `isIntegrallyClosedIn_iff`, `isIntegrallyClosed_iff`, `instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure`, `instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure`, `isIntegrallyClosedOfFiniteExtension`, `isIntegrallyClosedIn_iff`, `isIntegrallyClosed_iff`, `isIntegrallyClosed_iff_isIntegralClosure`, `isIntegrallyClosed_iff_isIntegrallyClosedIn`, `isIntegrallyClosed_of_isLocalization`	38
Total	39

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegrallyClosedIn`	—	`AlgHom.isIntegrallyClosedIn` `AlgEquivClass.toAlgHomClass` `instAlgEquivClass` `injective`

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegrallyClosedIn` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `funLike`	`IsIntegrallyClosedIn`	—	`Function.Injective.of_comp` `commutes` `isIntegral_algHom_iff`

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_iff` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow`	—	`IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `IsIntegrallyClosed.pow_dvd_pow_iff`

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIntegrallyClosed` 📖	mathematical	—	`IsIntegrallyClosed` `EuclideanDomain.toCommRing` `toEuclideanDomain`	—	`isIntegrallyClosed_iff` `instIsFractionRing`

IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isIntegralClosure_of_isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegralClosure` `CommRing.toCommSemiring`	—	`IsScalarTower.algebraMap_eq` `algebraMap_injective` `isIntegral_iff` `IsIntegral.tower_top` `isIntegral_algebraMap_iff` `IsScalarTower.algebraMap_apply` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass`
`of_isIntegrallyClosed` 📖	mathematical	—	`IsIntegralClosure` `CommRing.toCommSemiring`	—	`of_isIntegrallyClosedIn` `IsIntegrallyClosed.instIsIntegralClosure`
`of_isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegralClosure` `CommRing.toCommSemiring`	—	`algebraMap_injective` `isIntegral_iff` `IsIntegral.tower_top` `IsIntegral.map` `IsScalarTower.right` `AlgHom.algHomClass` `IsScalarTower.left` `Algebra.IsIntegral.isIntegral`

IsIntegrallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_eq_of_integral` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsIntegralClosure.isIntegral_iff` `instIsIntegralClosure`
`exists_algebraMap_eq_of_isIntegral_pow` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow` `instIsIntegralClosure`
`exists_algebraMap_eq_of_pow_mem_subalgebra` 📖	mathematical	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Subalgebra.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Subalgebra.toAlgebra` `Algebra.id`	—	`IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra` `instIsIntegralClosure`
`instIsIntegralClosure` 📖	mathematical	—	`IsIntegralClosure` `CommRing.toCommSemiring`	—	`isIntegrallyClosed_iff_isIntegralClosure`
`integralClosure_eq_bot` 📖	mathematical	—	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`integralClosure_eq_bot_iff`
`integralClosure_eq_bot_iff` 📖	mathematical	—	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsIntegrallyClosed`	—	`IsIntegrallyClosedIn.integralClosure_eq_bot_iff` `IsFractionRing.injective` `isIntegrallyClosed_iff_isIntegrallyClosedIn`
`isIntegral_iff` 📖	mathematical	—	`IsIntegral` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsIntegrallyClosedIn.isIntegral_iff` `instIsIntegralClosure`
`of_equiv` 📖	mathematical	—	`IsIntegrallyClosed`	—	`Localization.isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `isIntegrallyClosed_iff` `IsIntegral.tower_top` `isIntegral_algEquiv` `IsFractionRing.algEquivOfAlgEquiv_algebraMap` `AlgEquiv.symm_apply_eq`
`of_isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegrallyClosed`	—	`Function.Injective.isDomain` `instIsDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective` `Localization.isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `isIntegrallyClosed_iff` `RingHom.injective` `DivisionRing.isSimpleRing` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AlgHom.commutes` `IsIntegralClosure.isIntegral_iff` `IsIntegral.map` `IsScalarTower.left` `AlgHom.algHomClass`
`of_isIntegrallyClosed_of_isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegrallyClosed`	—	`IsIntegralClosure.of_isIntegralClosure_of_isIntegrallyClosedIn` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `of_isIntegrallyClosedIn` `FractionRing.instFaithfulSMul`
`pow_dvd_pow_iff` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`zero_pow` `MulZeroClass.zero_mul` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `Localization.isLocalization` `IsDomain.toNontrivial` `Polynomial.monic_X_pow_sub_C` `Polynomial.eval₂_sub` `Polynomial.eval₂_X_pow` `div_pow` `Polynomial.eval₂_C` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `Localization.instNoZeroDivisors` `FractionRing.instNontrivial` `sub_self` `algebraMap_eq_of_integral` `mul_div_cancel₀` `pow_dvd_pow_of_dvd`

IsIntegrallyClosedIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_eq_of_integral` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsIntegralClosure.isIntegral_iff`
`exists_algebraMap_eq_of_isIntegral_pow` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`isIntegral_iff` `IsIntegral.of_pow`
`exists_algebraMap_eq_of_pow_mem_subalgebra` 📖	mathematical	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Subalgebra.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Subalgebra.toAlgebra` `Algebra.id`	—	`exists_algebraMap_eq_of_isIntegral_pow` `isIntegral_iff`
`inst` 📖	mathematical	—	`IsIntegrallyClosedIn` `Algebra.id` `CommRing.toCommSemiring`	—	`Algebra.IsIntegral.of_finite` `Module.Finite.self`
`integralClosure_eq_bot` 📖	mathematical	—	`integralClosure` `Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`integralClosure_eq_bot_iff` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero`
`integralClosure_eq_bot_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`integralClosure` `Bot.bot` `Subalgebra` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsIntegrallyClosedIn`	—	`eq_bot_iff` `Set.mem_range` `Algebra.mem_bot` `isIntegral_algebraMap` `isIntegral_iff`
`isIntegral_iff` 📖	mathematical	—	`IsIntegral` `CommRing.toRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsIntegralClosure.isIntegral_iff`
`of_isIntegralClosure` 📖	mathematical	—	`IsIntegrallyClosedIn`	—	`IsIntegralClosure.isIntegral_algebra` `IsIntegralClosure.tower_top`

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integralClosure_le_iff` 📖	mathematical	—	`Subring` `CommRing.toRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Subalgebra.toSubring` `integralClosure` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `Subalgebra.instSMulMemClass` `SubringClass.toSubsemiringClass` `isIntegrallyClosedIn_iff` `instSubringClass` `IsScalarTower.of_algebraMap_eq` `IsIntegral.tower_top`
`integralClosure_subring_le_iff` 📖	mathematical	—	`Subring` `CommRing.toRing` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Subalgebra.toSubring` `SetLike.instMembership` `SubringClass.toCommRing` `Algebra.ofSubsemiring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SubringClass.toSubsemiringClass` `integralClosure` `ofClass`	—	`SubringClass.toSubsemiringClass` `integralClosure_le_iff` `SetLike.le_def` `instIsConcreteLE`
`isIntegrallyClosedIn_iff` 📖	mathematical	—	`IsIntegrallyClosedIn` `SetLike.instMembership` `SubringClass.toCommRing` `Algebra.ofSubsemiring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SubringClass.toSubsemiringClass` `CommRing.toRing`	—	`SubringClass.toSubsemiringClass` `isIntegrallyClosedIn_iff` `FaithfulSMul.algebraMap_injective` `Subsemiring.instFaithfulSMulSubtypeMem` `instFaithfulSMul` `Subtype.range_val`
`isIntegrallyClosed_iff` 📖	mathematical	—	`IsIntegrallyClosed` `SetLike.instMembership` `SubringClass.toCommRing`	—	`SubringClass.toSubsemiringClass` `isIntegrallyClosed_iff` `Subtype.range_val`

(root)

Definitions

Name	Category	Theorems
`IsIntegrallyClosedIn` 📖	MathDef	10 math math: `IsIntegrallyClosedIn.inst`, `instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure`, `IsIntegrallyClosedIn.of_isIntegralClosure`, `AlgEquiv.isIntegrallyClosedIn`, `instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure`, `IsIntegrallyClosedIn.integralClosure_eq_bot_iff`, `isIntegrallyClosedIn_iff`, `AlgHom.isIntegrallyClosedIn`, `isIntegrallyClosed_iff_isIntegrallyClosedIn`, `Subring.isIntegrallyClosedIn_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure` 📖	mathematical	—	`IsIntegrallyClosedIn` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`isIntegrallyClosedIn_iff` `FaithfulSMul.algebraMap_injective` `Subalgebra.instFaithfulSMulSubtypeMem` `instFaithfulSMul` `isIntegral_trans` `IsScalarTower.subalgebra'` `IsScalarTower.right` `integralClosure.AlgebraIsIntegral`
`instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure` 📖	mathematical	—	`IsIntegrallyClosedIn` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subalgebra.toSubring` `integralClosure` `Subring.toCommRing` `Algebra.ofSubring` `Algebra.id` `CommRing.toCommSemiring`	—	`instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure`
`isIntegrallyClosedIn_iff` 📖	mathematical	—	`IsIntegrallyClosedIn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`isIntegral_algebraMap`
`isIntegrallyClosed_iff` 📖	mathematical	—	`IsIntegrallyClosed` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`isIntegrallyClosed_iff_isIntegrallyClosedIn` `IsFractionRing.injective`
`isIntegrallyClosed_iff_isIntegralClosure` 📖	mathematical	—	`IsIntegrallyClosed` `IsIntegralClosure` `CommRing.toCommSemiring`	—	`isIntegrallyClosed_iff_isIntegrallyClosedIn`
`isIntegrallyClosed_iff_isIntegrallyClosedIn` 📖	mathematical	—	`IsIntegrallyClosed` `IsIntegrallyClosedIn`	—	`AlgEquiv.isIntegrallyClosedIn` `Localization.isLocalization`
`isIntegrallyClosed_of_isLocalization` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsIntegrallyClosed`	—	`Localization.isLocalization` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq'` `RingHom.algebraMap_toAlgebra` `IsLocalization.map_comp` `RingHomCompTriple.comp_eq` `RingHomCompTriple.ids` `IsFractionRing.isFractionRing_of_isDomain_of_isLocalization` `isIntegrallyClosed_iff_isIntegralClosure` `IsFractionRing.injective` `IsIntegral.exists_multiple_integral_of_isLocalization` `isIntegrallyClosed_iff` `IsLocalization.lift_mk'_spec` `RingHom.comp_id` `Algebra.smul_def` `Submonoid.mk_smul` `isIntegral_algebraMap`

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegrallyClosedOfFiniteExtension` 📖	mathematical	—	`IsIntegrallyClosed` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing`	—	`IsIntegrallyClosed.integralClosure_eq_bot_iff` `isFractionRing_of_finite_extension` `integralClosure_idem`

---

← Back to Index