Documentation Verification Report

LocalSubring

📁 Source: Mathlib/RingTheory/Valuation/LocalSubring.lean

Statistics

Metric	Count
Definitions `LocalSubring`, `toLocalSubring`	2
Theorems `image_subset_nonunits_valuationSubring`, `exists_factor_valuationRing`, `eq_iInf_of_isIntegrallyClosedIn`, `exists_le_valuationSubring`, `exists_le_valuationSubring_of_isIntegrallyClosedIn`, `exists_valuationRing_of_isMax`, `isMax_iff`, `map_maximalIdeal_eq_top_of_isMax`, `mem_of_isMax_of_isIntegral`, `eq_iInf_of_isIntegrallyClosedIn`, `exists_le_valuationSubring_of_isIntegrallyClosedIn`, `isMax_toLocalSubring`, `toLocalSubring_injective`, `bijective_rangeRestrict_comp_of_valuationRing`, `iInf_valuationSubring_superset`, `instIsIntegrallyClosedSubtypeMemSubring`, `instIsIntegrallyClosedSubtypeMemValuationSubring`	17
Total	19

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_subset_nonunits_valuationSubring` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Preorder.toLE` `PartialOrder.toPreorder` `Subring.instPartialOrder` `ValuationSubring.toSubring` `Set` `Set.instHasSubset` `Set.image` `SetLike.instMembership` `Subring.instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subring.toRing` `RingHom.instFunLike` `Subring.subtype` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalSubring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `NonUnitalSubring.instSetLike` `ValuationSubring.nonunits`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `exists_le_maximal` `IsMaximal.isPrime'` `LocalSubring.exists_le_valuationSubring` `LE.le.trans` `LocalSubring.le_ofPrime` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `ValuationSubring.image_maximalIdeal` `HasSubset.Subset.trans` `Set.instIsTransSubset` `LocalSubring.isLocalRing` `IsLocalization.AtPrime.map_eq_maximalIdeal` `LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime` `map_map` `mem_map_of_mem` `Set.image_mono` `map_mono` `List.TFAE.out` `RingHom.instRingHomClass` `IsLocalRing.local_hom_TFAE`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_factor_valuationRing` 📖	mathematical	—	`IsLocalHom` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `ValuationSubring.toSubring` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubsemiringClass.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `RingHom.codRestrict`	—	`EuclideanDomain.toNontrivial` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `LocalSubring.exists_le_valuationSubring` `RingHom.isLocalHom_comp` `IsLocalHom.of_surjective` `Subring.instNontrivialSubtypeMem` `RingHom.rangeRestrict_surjective`

LocalSubring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iInf_of_isIntegrallyClosedIn` 📖	mathematical	—	`toSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `iInf` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `LocalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toLocalSubring` `Subring.instInfSet` `ValuationSubring.toSubring`	—	`le_antisymm` `le_iInf` `of_not_not` `exists_le_valuationSubring_of_isIntegrallyClosedIn` `iInf_le_of_le` `le_rfl`
`exists_le_valuationSubring` 📖	mathematical	—	`LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toLocalSubring`	—	`zorn_le_nonempty_Ici₀` `Directed.mono_comp` `toSubring_mono` `IsChain.directed` `instReflLe` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Subring.instNontrivialSubtypeMem` `EuclideanDomain.toNontrivial` `Subring.mem_iSup_of_directed` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `le_iSup` `IsLocalRing.isUnit_or_isUnit_of_add_one` `isLocalRing` `isUnit_iff_exists_inv` `SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem` `SubsemiringClass.toSubmonoidClass` `instIsDedekindFiniteMonoid` `IsLocalHom.map_nonunit` `le_rfl` `exists_valuationRing_of_isMax`
`exists_le_valuationSubring_of_isIntegrallyClosedIn` 📖	mathematical	`Subring` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Subring.instSetLike` `toSubring`	`LocalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toLocalSubring` `ValuationSubring` `ValuationSubring.instSetLike`	—	`eq_or_ne` `Subring.zero_mem` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Algebra.subset_adjoin` `isLocalRing` `Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal` `of_not_not` `sub_sub_cancel` `sub_mem` `Submodule.addSubgroupClass` `Subring.isIntegrallyClosedIn_iff` `Polynomial.Monic.leadingCoeff` `Polynomial.leadingCoeff_mul` `Subring.instNoZeroDivisorsSubtypeMem` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.leadingCoeff_C` `IsUnit.val_inv_mul` `Polynomial.eval₂_mul` `Polynomial.eval₂_C` `map_units_inv` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Subring.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `EuclideanDomain.toNontrivial` `Ideal.image_subset_nonunits_valuationSubring` `Subalgebra.algebraMap_mem` `List.TFAE.out` `IsLocalRing.local_hom_TFAE` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `ValuationSubring.image_maximalIdeal` `le_self_add` `Submodule.instCanonicallyOrderedAdd` `Ideal.mem_map_of_mem` `ValuationSubring.inv_mem_nonunits_iff` `le_add_self` `Ideal.subset_span`
`exists_valuationRing_of_isMax` 📖	mathematical	`IsMax` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`ValuationSubring.toLocalSubring`	—	`mem_of_isMax_of_isIntegral` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `Subalgebra.instSMulMemClass` `Algebra.self_mem_adjoin_singleton` `isLocalRing` `Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top` `Ideal.IsMaximal.ne_top` `IsLocalRing.maximalIdeal.isMaximal` `top_unique` `Algebra.subset_adjoin` `LE.le.trans` `LT.lt.le` `Eq.ge` `map_maximalIdeal_eq_top_of_isMax` `le_self_add` `Submodule.instCanonicallyOrderedAdd` `of_not_not` `sub_sub_cancel` `sub_mem` `Submodule.addSubgroupClass` `Polynomial.Monic.leadingCoeff` `Polynomial.leadingCoeff_mul` `Subring.instNoZeroDivisorsSubtypeMem` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.leadingCoeff_C` `IsUnit.val_inv_mul` `Polynomial.eval₂_mul` `Polynomial.eval₂_C` `map_units_inv` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Subring.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `EuclideanDomain.toNontrivial`
`isMax_iff` 📖	mathematical	—	`IsMax` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toLocalSubring`	—	`exists_valuationRing_of_isMax` `ValuationSubring.isMax_toLocalSubring`
`map_maximalIdeal_eq_top_of_isMax` 📖	mathematical	`IsMax` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Subring` `CommRing.toRing` `Preorder.toLT` `Subring.instPartialOrder` `toSubring`	`Ideal.map` `SetLike.instMembership` `Subring.instSetLike` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subring.toRing` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSubringClass` `RingHom.instFunLike` `Subring.inclusion` `LT.lt.le` `IsLocalRing.maximalIdeal` `isLocalRing` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `LT.lt.le` `isLocalRing` `Ideal.exists_le_maximal` `Ideal.IsMaximal.isPrime'` `LE.le.trans` `le_ofPrime` `List.TFAE.out` `RingHom.instRingHomClass` `IsLocalRing.local_hom_TFAE` `IsLocalization.AtPrime.map_eq_maximalIdeal` `instAtPrimeSubtypeMemSubringToSubringOfPrime` `Ideal.map_map` `le_refl` `Ideal.map_mono` `LT.lt.not_ge` `IsMax.eq_of_le`
`mem_of_isMax_of_isIntegral` 📖	—	`IsMax` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsIntegral` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `toSubring` `Subring.toCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Algebra.ofSubring` `Algebra.id` `CommRing.toCommSemiring`	—	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Algebra.IsIntegral.adjoin` `RingHom.instRingHomClass` `isLocalRing` `Ideal.exists_ideal_over_maximal_of_isIntegral` `IsLocalRing.maximalIdeal.isMaximal` `IsLocalRing.le_maximalIdeal` `FaithfulSMul.ker_algebraMap_eq_bot` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Subring.instIsDomainSubtypeMem` `instIsDomain` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `EuclideanDomain.toNontrivial` `Subalgebra.instIsTorsionFree` `FaithfulSMul.to_isTorsionFree` `Subring.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `Subring.instNontrivialSubtypeMem` `Ideal.instNontrivial` `Ideal.IsMaximal.isPrime'` `algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSMulMemClass` `IsMax.eq_of_le` `LE.le.trans` `le_ofPrime` `List.TFAE.out` `IsLocalRing.local_hom_TFAE` `IsLocalization.AtPrime.map_eq_maximalIdeal` `instAtPrimeSubtypeMemSubringToSubringOfPrime` `Ideal.map_map` `le_refl` `Ideal.map_mono` `Ideal.map_le_iff_le_comap` `Eq.ge` `Algebra.self_mem_adjoin_singleton`

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iInf_of_isIntegrallyClosedIn` 📖	mathematical	—	`iInf` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toSubring` `instInfSet`	—	`le_antisymm` `le_iInf` `of_not_not` `exists_le_valuationSubring_of_isIntegrallyClosedIn` `iInf_le_of_le` `le_rfl`
`exists_le_valuationSubring_of_isIntegrallyClosedIn` 📖	mathematical	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `ValuationSubring.toSubring` `ValuationSubring` `ValuationSubring.instSetLike`	—	`eq_or_ne` `zero_mem` `SubringClass.toSubsemiringClass` `instSubringClass` `Algebra.subset_adjoin` `Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top` `bot_ne_top` `Ideal.instNontrivial` `instNontrivialSubtypeMem` `EuclideanDomain.toNontrivial` `top_unique` `LE.le.trans` `Eq.ge` `le_add_self` `Submodule.instCanonicallyOrderedAdd` `isIntegrallyClosedIn_iff` `Ideal.image_subset_nonunits_valuationSubring` `Subalgebra.algebraMap_mem` `ValuationSubring.inv_mem_nonunits_iff` `Ideal.subset_span`

ValuationSubring

Definitions

Name	Category	Theorems
`toLocalSubring` 📖	CompOp	7 math math: `LocalSubring.isMax_iff`, `isMax_toLocalSubring`, `LocalSubring.exists_le_valuationSubring`, `LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn`, `toLocalSubring_injective`, `LocalSubring.eq_iInf_of_isIntegrallyClosedIn`, `LocalSubring.exists_valuationRing_of_isMax`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMax_toLocalSubring` 📖	mathematical	—	`IsMax` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `LocalSubring.instPartialOrder` `toLocalSubring`	—	`Eq.ge` `LocalSubring.toSubring_injective` `LE.le.antisymm` `mem_or_inv_mem'` `zero_mem` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `isUnit_iff_exists_inv` `SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem` `SubsemiringClass.toSubmonoidClass` `instIsDedekindFiniteMonoid` `inv_mul_cancel₀` `IsLocalHom.map_nonunit` `inv_mul_eq_iff_eq_mul₀` `mul_one`
`toLocalSubring_injective` 📖	mathematical	—	`ValuationSubring` `LocalSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toLocalSubring`	—	`toSubring_injective`

(root)

Definitions

Name	Category	Theorems
`LocalSubring` 📖	CompData	9 math math: `LocalSubring.isMax_iff`, `ValuationSubring.isMax_toLocalSubring`, `LocalSubring.toSubring_mono`, `LocalSubring.exists_le_valuationSubring`, `LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedIn`, `ValuationSubring.toLocalSubring_injective`, `LocalSubring.eq_iInf_of_isIntegrallyClosedIn`, `LocalSubring.le_def`, `LocalSubring.toSubring_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_rangeRestrict_comp_of_valuationRing` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `algebraMap`	`Function.Bijective` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `DFunLike.coe` `RingHom` `Ring.toSemiring` `Subring.toRing` `RingHom.instFunLike` `RingHom.rangeRestrict`	—	`Function.Injective.of_comp` `IsFractionRing.injective` `ValuationRing.isInteger_or_isInteger` `EuclideanDomain.toNontrivial` `ValuationSubring.isMax_toLocalSubring` `IsUnit.of_map` `IsLocalHom.map_nonunit` `IsLocalHom.of_surjective` `Subring.instNontrivialSubtypeMem` `RingHom.rangeRestrict_surjective` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`iInf_valuationSubring_superset` 📖	mathematical	—	`iInf` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `Set` `Set.instHasSubset` `SetLike.coe` `Subring.instSetLike` `ValuationSubring.toSubring` `Subring.instInfSet` `Subalgebra.toSubring` `SetLike.instMembership` `Subring.closure` `Subring.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.ofSubring` `Algebra.id` `CommRing.toCommSemiring` `integralClosure`	—	`iInf_subtype` `iInf_congr_Prop` `IsIntegralClosure.of_isIntegrallyClosed` `ValuationSubring.instIsFractionRingSubtypeMem` `instIsIntegrallyClosedSubtypeMemValuationSubring` `IsScalarTower.left` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `Algebra.IsIntegral.of_finite` `Module.Finite.self` `Subring.integralClosure_subring_le_iff` `Subring.closure_le` `Subring.eq_iInf_of_isIntegrallyClosedIn` `instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure`
`instIsIntegrallyClosedSubtypeMemSubring` 📖	mathematical	—	`IsIntegrallyClosed` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `ValuationSubring.toSubring` `Subring.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ValuationSubring.integer_valuation` `Valuation.Integers.isIntegrallyClosed_integers`
`instIsIntegrallyClosedSubtypeMemValuationSubring` 📖	mathematical	—	`IsIntegrallyClosed` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `ValuationSubring.instCommRingSubtypeMem`	—	`instIsIntegrallyClosedSubtypeMemSubring`

---

← Back to Index