Documentation Verification Report

IntegralClosure

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_is_basis_integral`, `finite`, `isDedekindDomain`, `isLocalization`, `isLocalization_of_isSeparable`, `isNoetherian`, `isNoetherianRing`, `module_free`, `range_le_span_dualBasis`, `rank`, `exists_integral_multiples`, `isDedekindDomain`, `isDedekindDomain_fractionRing`, `isNoetherianRing`, `integralClosure_le_span_dualBasis`	15
Total	15

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_is_basis_integral` 📖	mathematical	—	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Module.Basis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Module.Basis.instFunLike`	—	`isNoetherian_of_isNoetherianRing_of_finite` `IsDedekindRing.toIsNoetherian` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `exists_integral_multiples` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `IsScalarTower.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsFractionRing.injective` `smulCommClass_self` `IsScalarTower.left` `RingHomInvPair.ids` `AddHom.map_add'` `LinearMap.map_smul'` `inv_mul_cancel_left₀` `mul_inv_cancel_left₀` `Algebra.smul_def`

IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Module.IsNoetherian.finite` `isNoetherian`
`isDedekindDomain` 📖	mathematical	—	`IsDedekindDomain`	—	`isFractionRing_of_finite_extension` `isIntegral_algebra` `isNoetherianRing` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `IsDedekindRing.toIsNoetherian` `Ring.DimensionLEOne.isIntegralClosure` `IsDomain.toNontrivial` `IsDedekindRing.toDimensionLEOne` `isIntegrallyClosed_iff` `isIntegral_trans` `algebraMap_mk'`
`isLocalization` 📖	mathematical	—	`IsLocalization` `CommRing.toCommSemiring` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isUnit_iff_ne_zero` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_injective` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `MulEquiv.isDomain` `instIsDomainSubtypeMemSubalgebraIntegralClosure` `instIsDomain` `integralClosure.isIntegralClosure` `IsScalarTower.subalgebra'` `IsScalarTower.right` `isTorsionFree` `Module.IsTorsionFree.trans_faithfulSMul` `IsFractionRing.instFaithfulSMul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors` `IsIntegral.exists_multiple_integral_of_isLocalization` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `isIntegral_iff` `SetLike.coe_mem` `IsScalarTower.algebraMap_apply` `mul_comm` `Submonoid.smul_def` `Algebra.smul_def`
`isLocalization_of_isSeparable` 📖	mathematical	—	`IsLocalization` `CommRing.toCommSemiring` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isLocalization` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isNoetherian` 📖	mathematical	—	`IsNoetherian` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`FiniteDimensional.exists_is_basis_integral` `Finite.of_fintype` `traceForm_nondegenerate` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul'` `RingHomCompTriple.ids` `range_le_span_dualBasis` `isNoetherian_of_ker_bot` `isNoetherian_span_of_finite` `Set.finite_range` `LinearMap.ker_comp` `Submodule.ker_inclusion` `Submodule.comap_bot` `LinearMap.mem_range_self` `LinearMap.ker_codRestrict` `LinearMap.ker_eq_bot_of_injective` `algebraMap_injective`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`isNoetherianRing_iff` `isNoetherian_of_tower` `IsScalarTower.right` `isNoetherian`
`module_free` 📖	mathematical	—	`Module.Free` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Module.free_of_finite_type_torsion_free'` `Module.IsNoetherian.finite` `isNoetherian` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `IsDedekindRing.toIsNoetherian` `isTorsionFree`
`range_le_span_dualBasis` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Module.Basis.instFunLike`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHom.id` `RingHomSurjective.ids` `LinearMap.restrictScalars` `Semiring.toModule` `LinearMap.IsScalarTower.compatibleSMul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.linearMap` `Submodule.span` `Set.range` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `LinearMap.BilinForm.dualBasis` `Algebra.traceForm` `traceForm_nondegenerate`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul'` `traceForm_nondegenerate` `LinearMap.BilinForm.dualSubmodule_span_of_basis` `LinearMap.BilinForm.le_flip_dualSubmodule` `Submodule.span_le` `Submodule.mem_one` `IsIntegrallyClosed.isIntegral_iff` `Algebra.isIntegral_trace` `IsIntegral.mul` `IsIntegral.algebraMap` `isIntegral`
`rank` 📖	mathematical	—	`Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semifield.toCommSemiring`	—	`module_free` `isLocalization` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `IsDedekindRing.toIsNoetherian` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `IsDomain.toNontrivial` `Module.finrank_eq_card_basis`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_integral_multiples` 📖	mathematical	—	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.toSMul` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`IsLocalization.isAlgebraic` `IsDomain.toNontrivial` `Algebra.IsAlgebraic.trans` `IsDomain.to_noZeroDivisors` `instIsDomain` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsAlgebraic.exists_integral_multiples`
`integralClosure_le_span_dualBasis` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Module.Basis.instFunLike`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderEmbedding` `Subalgebra` `Subalgebra.instPartialOrder` `instFunLikeOrderEmbedding` `Subalgebra.toSubmodule` `integralClosure` `Submodule.span` `Set.range` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `LinearMap.BilinForm.dualBasis` `Algebra.traceForm` `traceForm_nondegenerate`	—	`le_trans` `RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul'` `IsScalarTower.subalgebra'` `IsScalarTower.right` `traceForm_nondegenerate` `IsIntegralClosure.range_le_span_dualBasis` `integralClosure.isIntegralClosure`

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDedekindDomain` 📖	mathematical	—	`IsDedekindDomain` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing`	—	`IsIntegralClosure.isDedekindDomain` `isIntegralClosure` `IsScalarTower.subalgebra'` `IsScalarTower.right` `instIsDomainSubtypeMemSubalgebraIntegralClosure` `instIsDomain`
`isDedekindDomain_fractionRing` 📖	mathematical	—	`IsDedekindDomain` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing`	—	`IsScalarTower.right` `IsDomain.toNontrivial` `IsDomain.to_noZeroDivisors` `isDedekindDomain` `Localization.isLocalization`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toSemiring`	—	`IsIntegralClosure.isNoetherianRing` `isIntegralClosure` `IsScalarTower.subalgebra'` `IsScalarTower.right`

---

← Back to Index