ExtendToLocalization

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

Statistics

Metric	Count
Definitions extendToLocalization	1
Theorems extendToLocalization_apply_map_apply, extendToLocalization_mk'	2
Total	3

Valuation

Definitions

Name	Category	Theorems
extendToLocalization 📖	CompOp	3 math math: IsDedekindDomain.HeightOneSpectrum.valuation_def, extendToLocalization_mk', extendToLocalization_apply_map_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendToLocalization_apply_map_apply 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Ideal.primeCompl supp LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instIsPrimeSuppOfNontrivialOfNoZeroDivisors GroupWithZero.toNontrivial CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero GroupWithZero.noZeroDivisors	DFunLike.coe Valuation CommRing.toRing instFunLike extendToLocalization RingHom RingHom.instFunLike algebraMap	—	instIsPrimeSuppOfNontrivialOfNoZeroDivisors GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors Submonoid.LocalizationMap.lift_eq
extendToLocalization_mk' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Ideal.primeCompl supp LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instIsPrimeSuppOfNontrivialOfNoZeroDivisors GroupWithZero.toNontrivial CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero GroupWithZero.noZeroDivisors	DFunLike.coe Valuation CommRing.toRing instFunLike extendToLocalization IsLocalization.mk' MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid SetLike.instMembership Submonoid.instSetLike	—	instIsPrimeSuppOfNontrivialOfNoZeroDivisors GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors Submonoid.instSubmonoidClass Submonoid.LocalizationMap.lift_mk' Units.val_inv_eq_inv_val

---

← Back to Index