Documentation Verification Report

Extension

📁 Source: Mathlib/RingTheory/Localization/AtPrime/Extension.lean

Statistics

Metric	Count
Definitions `primesOverEquivPrimesOver`, `equivQuotientMapOfIsMaximal`	2
Theorems `primesOverEquivPrimesOver_apply`, `primesOverEquivPrimesOver_inertiagDeg_eq`, `primesOverEquivPrimesOver_ramificationIdx_eq`, `primesOverEquivPrimesOver_symm_apply`, `algebraMap_equivQuotMaximalIdeal_symm_apply`, `equivQuotientMapMaximalIdeal_apply_mk`, `equivQuotientMapOfIsMaximal_apply_mk`, `equivQuotientMapOfIsMaximal_symm_apply_mk`, `exists_algebraMap_quot_eq_of_mem_quot`, `inertiaDeg_map_eq_inertiaDeg`, `liesOver_comap_of_liesOver`, `liesOver_map_of_liesOver`, `mem_primesOver_of_isPrime`, `ramificationIdx_map_eq_ramificationIdx`	14
Total	16

IsDedekindDomain

Definitions

Name	Category	Theorems
`primesOverEquivPrimesOver` 📖	CompOp	4 math math: `primesOverEquivPrimesOver_inertiagDeg_eq`, `primesOverEquivPrimesOver_apply`, `primesOverEquivPrimesOver_ramificationIdx_eq`, `primesOverEquivPrimesOver_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primesOverEquivPrimesOver_apply` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Ideal.primesOver` `IsLocalRing.maximalIdeal` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `primesOverEquivPrimesOver` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`primesOverEquivPrimesOver_inertiagDeg_eq` 📖	mathematical	—	`Ideal.inertiaDeg` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Ideal.primesOver` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `primesOverEquivPrimesOver`	—	`Ring.DimensionLEOne.maximalOfPrime` `IsDedekindDomainDvr.ring_dimensionLEOne` `toIsDomain` `isDedekindDomainDvr` `Ideal.ne_bot_of_mem_primesOver` `IsDomain.toNontrivial` `Subtype.prop` `Ideal.primesOver.isPrime` `IsLocalization.AtPrime.liesOver_map_of_liesOver` `Ideal.primesOver.liesOver` `IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg`
`primesOverEquivPrimesOver_ramificationIdx_eq` 📖	mathematical	—	`Ideal.ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `IsLocalRing.maximalIdeal` `Ideal` `Set` `Set.instMembership` `Ideal.primesOver` `DFunLike.coe` `OrderIso` `Set.Elem` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `primesOverEquivPrimesOver`	—	`IsLocalization.AtPrime.ramificationIdx_map_eq_ramificationIdx` `Ideal.primesOver.liesOver` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `toIsDomain` `Ideal.primesOver.isPrime`
`primesOverEquivPrimesOver_symm_apply` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Ideal.primesOver` `DFunLike.coe` `OrderIso` `Set.Elem` `IsLocalRing.maximalIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLikeOrderIso` `OrderIso.symm` `primesOverEquivPrimesOver` `Ideal.comap` `RingHom` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	—

IsLocalization.AtPrime

Definitions

Name	Category	Theorems
`equivQuotientMapOfIsMaximal` 📖	CompOp	3 math math: `equivQuotientMapOfIsMaximal_apply_mk`, `equivQuotientMapOfIsMaximal_symm_apply_mk`, `algebraMap_equivQuotMaximalIdeal_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_equivQuotMaximalIdeal_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Semiring.toNonAssocSemiring` `Ideal.Quotient.commSemiring` `Ideal.Quotient.semiring` `RingHom.instFunLike` `algebraMap` `Ideal.Quotient.algebraOfLiesOver` `RingEquiv` `IsLocalRing.maximalIdeal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivQuotMaximalIdeal` `Ideal.map` `equivQuotientMapOfIsMaximal`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `IsLocalization.mk'_surjective` `Ideal.IsMaximal.isPrime'` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `Algebra.mem_algebraMapSubmonoid_of_mem` `IsLocalization.algebraMap_mk'`
`equivQuotientMapMaximalIdeal_apply_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivQuotientMapMaximalIdeal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1`
`equivQuotientMapOfIsMaximal_apply_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivQuotientMapOfIsMaximal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1`
`equivQuotientMapOfIsMaximal_symm_apply_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivQuotientMapOfIsMaximal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `IsLocalization.mk'` `Algebra.algebraMapSubmonoid` `Ideal.primeCompl` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Ideal.Quotient.field` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`isPrime_map_of_liesOver` `Ideal.IsMaximal.isPrime'` `Ideal.instIsTwoSided_1` `Iff.not` `Ideal.Quotient.eq_zero_iff_mem` `Set.disjoint_left` `Ideal.disjoint_primeCompl_of_liesOver` `Subtype.prop` `RingEquiv.map_ne_zero_iff` `RingEquiv.symm_apply_eq` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Ideal.Quotient.isDomain` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `mul_assoc` `inv_mul_cancel₀` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `mul_one` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsLocalization.mk'_spec` `Ideal.Quotient.mk_algebraMap`
`exists_algebraMap_quot_eq_of_mem_quot` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.map` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `IsLocalization.exists_mk'_eq` `IsScalarTower.algebraMap_eq` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Ideal.Quotient.eq_zero_iff_mem` `isPrime_map_of_liesOver` `Ideal.IsMaximal.isPrime'` `Set.disjoint_left` `Ideal.disjoint_primeCompl_of_liesOver` `Subtype.prop` `Ideal.mem_comap` `Ideal.comap_map_eq_self_of_isMaximal` `Ideal.IsPrime.ne_top` `Ideal.IsPrime.mem_or_mem` `mul_sub` `IsLocalization.mul_mk'_eq_mk'_of_mul` `IsLocalization.mk'_mul_cancel_left` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Ideal.IsPrime.ne_top'` `Ideal.Quotient.eq` `mul_comm` `inv_mul_cancel_right₀` `Iff.not`
`inertiaDeg_map_eq_inertiaDeg` 📖	mathematical	—	`Ideal.inertiaDeg` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Ideal.inertiaDeg_algebraMap` `IsLocalRing.maximalIdeal.isMaximal` `Algebra.finrank_eq_of_equiv_equiv` `Ideal.Quotient.ringHom_ext` `Ideal.instIsTwoSided_1` `RingHom.ext` `algebraMap_equivQuotMaximalIdeal_symm_apply`
`liesOver_comap_of_liesOver` 📖	mathematical	—	`Ideal.LiesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`liesOver_maximalIdeal` `Ideal.LiesOver.trans` `Ideal.comap_liesOver` `AlgHom.algHomClass`
`liesOver_map_of_liesOver` 📖	mathematical	—	`Ideal.LiesOver` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.maximalIdeal`	—	`Ideal.liesOver_iff` `map_eq_maximalIdeal` `Ideal.over_def` `Ideal.under_map_eq_map_under` `IsLocalRing.maximalIdeal.isMaximal` `Ideal.IsPrime.ne_top` `isPrime_map_of_liesOver`
`mem_primesOver_of_isPrime` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Ideal.primesOver` `IsLocalRing.maximalIdeal`	—	`Ideal.IsMaximal.isPrime'` `Ideal.liesOver_iff` `IsLocalRing.eq_maximalIdeal` `Ideal.IsMaximal.under`
`ramificationIdx_map_eq_ramificationIdx` 📖	mathematical	—	`Ideal.ramificationIdx` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `IsLocalRing.maximalIdeal` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`map_eq_maximalIdeal` `Ideal.map_ne_bot_of_ne_bot` `IsLocalRing.toNontrivial` `isPrime_map_of_liesOver` `Ideal.map_bot` `RingHom.instRingHomClass` `Ideal.ramificationIdx_bot'` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.map_le_iff_le_comap` `le_of_eq` `Ideal.liesOver_iff` `liesOver_map_of_liesOver` `Ideal.ramificationIdx_algebra_tower` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `le_rfl` `one_mul` `Ideal.ramificationIdx_map_self_eq_one` `Ideal.IsPrime.ne_top'` `mul_one`

---

← Back to Index