Basic

📁 Source: Mathlib/RingTheory/LocalProperties/Basic.lean

Statistics

Metric	Count
Definitions LocalizationPreserves, OfLocalizationMaximal, ContainsIdentities, HoldsForLocalization, HoldsForLocalizationAway, LocalizationAwayPreserves, LocalizationPreserves, OfLocalizationFiniteSpan, OfLocalizationFiniteSpanTarget, OfLocalizationPrime, OfLocalizationSpan, OfLocalizationSpanTarget, PropertyIsLocal, StableUnderCompositionWithLocalizationAway, StableUnderCompositionWithLocalizationAwaySource, StableUnderCompositionWithLocalizationAwayTarget	16
Theorems idealMap_eq_ofEq_comp_toLocalized₀, eq_of_localization_maximal, iInf_ker_le, le_of_localization_maximal, localized'_eq_map, localized₀_eq_restrictScalars_map, mem_of_localization_maximal, holdsForLocalizationAway, isLocalizationMap, localRingHom, mk, containsIdentities, of_bijective, isLocalization_map, localizationPreserves, of_isLocalization, and, respectsIso, away, and, mk, ofIsLocalization, ofIsLocalization', and, ofIsLocalization, ofLocalizationSpan, HoldsForLocalizationAway, StableUnderCompositionWithLocalizationAwayTarget, and, localizationAwayPreserves, ofLocalizationSpan, ofLocalizationSpanTarget, respectsIso, stableUnderCompositionWithLocalizationAway, respectsIso, and, ofLocalizationSpanTarget_iff_finite, ofLocalizationSpan_iff_finite, eq_zero_of_localization, ideal_eq_bot_of_localization, ideal_eq_bot_of_localization'	41
Total	57

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealMap_eq_ofEq_comp_toLocalized₀ 📖	mathematical	—	idealMap CommSemiring.toSemiring LinearMap.comp Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike toModule Submodule.localized₀ linearMap instIsLocalizedModuleLinearMapOfIsLocalization Submodule.restrictScalars toSMul IsScalarTower.right Ideal.map RingHom RingHom.instFunLike algebraMap Submodule.addCommMonoid Submodule.module RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.ofEq Ideal.localized₀_eq_restrictScalars_map Submodule.toLocalized₀	—	IsScalarTower.right

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_localization_maximal 📖	—	map Localization.AtPrime IsMaximal.isPrime' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—	IsMaximal.isPrime' le_antisymm le_of_localization_maximal Eq.le Eq.ge
iInf_ker_le 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iInf Submodule.instInfSet IsPrime RingHom.ker Localization.AtPrime RingHom OreLocalization.instSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike RingHom.instRingHomClass algebraMap OreLocalization.instAlgebra Algebra.id	—	RingHom.instRingHomClass mem_of_localization_maximal IsMaximal.isPrime' AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass IsLocalization.AtPrime.map_eq_top_of_not_le Localization.isLocalization
le_of_localization_maximal 📖	mathematical	Ideal Localization.AtPrime IsMaximal.isPrime' OreLocalization.instSemiring CommSemiring.toSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsMaximal.isPrime' mem_of_localization_maximal mem_map_of_mem
localized'_eq_map 📖	mathematical	—	Submodule.localized' NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule IsScalarTower.right Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization map RingHom RingHom.instFunLike algebraMap	—	IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization map.eq_1 span.eq_1 Submodule.localized'_eq_span Algebra.coe_linearMap
localized₀_eq_restrictScalars_map 📖	mathematical	—	Submodule.localized₀ NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Algebra.toModule Algebra.linearMap instIsLocalizedModuleLinearMapOfIsLocalization Submodule.restrictScalars Algebra.toSMul IsScalarTower.right map RingHom RingHom.instFunLike algebraMap	—	instIsLocalizedModuleLinearMapOfIsLocalization IsScalarTower.right localized'_eq_map
mem_of_localization_maximal 📖	mathematical	Localization.AtPrime IsMaximal.isPrime' Ideal OreLocalization.instSemiring CommSemiring.toSemiring primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule map RingHom RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id DFunLike.coe	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsMaximal.isPrime' Submodule.mem_of_localization_maximal IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization Localization.isLocalization localized'_eq_map

RingHom

Definitions

Name	Category	Theorems
ContainsIdentities 📖	MathDef	6 math math: HoldsForLocalizationAway.containsIdentities, Bijective.containsIdentities, IsStandardOpenImmersion.containsIdentities, finite_containsIdentities, Flat.containsIdentities, Etale.containsIdentities
HoldsForLocalization 📖	MathDef	3 math math: FormallyUnramified.holdsForLocalization, EssFiniteType.holdsForLocalization, HoldsForLocalization.mk
HoldsForLocalizationAway 📖	MathDef	13 math math: PropertyIsLocal.HoldsForLocalizationAway, finiteType_holdsForLocalizationAway, QuasiFinite.holdsForLocalizationAway, Smooth.holdsForLocalizationAway, locally_holdsForLocalizationAway, IsStandardOpenImmersion.holdsForLocalizationAway, isStandardSmooth_holdsForLocalizationAway, isStandardSmoothOfRelativeDimension_holdsForLocalizationAway, HoldsForLocalization.holdsForLocalizationAway, FormallySmooth.holdsForLocalizationAway, Flat.holdsForLocalizationAway, FormallyUnramified.holdsForLocalizationAway, finitePresentation_holdsForLocalizationAway
LocalizationAwayPreserves 📖	MathDef	4 math math: PropertyIsLocal.localizationAwayPreserves, locally_localizationAwayPreserves, LocalizationPreserves.away, LocalizationAwayPreserves.and
LocalizationPreserves 📖	MathDef	9 math math: isStandardSmoothOfRelativeDimension_localizationPreserves, FormallySmooth.localizationPreserves, finite_localizationPreserves, isStandardSmooth_localizationPreserves, IsStableUnderBaseChange.localizationPreserves, locally_localizationPreserves, finitePresentation_localizationPreserves, surjective_localizationPreserves, finiteType_localizationPreserves
OfLocalizationFiniteSpan 📖	MathDef	1 math math: ofLocalizationSpan_iff_finite
OfLocalizationFiniteSpanTarget 📖	MathDef	1 math math: ofLocalizationSpanTarget_iff_finite
OfLocalizationPrime 📖	MathDef	2 math math: FormallyUnramified.ofLocalizationPrime, Flat.ofLocalizationPrime
OfLocalizationSpan 📖	MathDef	11 math math: OfLocalizationSpan.mk, OfLocalizationSpan.and, Bijective.ofLocalizationSpan, isIntegral_ofLocalizationSpan, finiteType_ofLocalizationSpan, Etale.ofLocalizationSpan, OfLocalizationSpanTarget.ofLocalizationSpan, ofLocalizationSpan_iff_finite, finite_ofLocalizationSpan, PropertyIsLocal.ofLocalizationSpan, surjective_ofLocalizationSpan
OfLocalizationSpanTarget 📖	MathDef	11 math math: finiteType_ofLocalizationSpanTarget, QuasiFinite.ofLocalizationSpanTarget, ofLocalizationSpanTarget_iff_finite, PropertyIsLocal.ofLocalizationSpanTarget, Smooth.ofLocalizationSpanTarget, locally_ofLocalizationSpanTarget, FormallyUnramified.ofLocalizationSpanTarget, Flat.ofLocalizationSpanTarget, OfLocalizationSpanTarget.and, Etale.ofLocalizationSpanTarget, finitePresentation_ofLocalizationSpanTarget
PropertyIsLocal 📖	CompData	11 math math: QuasiFinite.propertyIsLocal, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty, Etale.propertyIsLocal, finiteType_isLocal, finitePresentation_isLocal, Smooth.propertyIsLocal, PropertyIsLocal.and, AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget, Flat.propertyIsLocal, FormallyUnramified.propertyIsLocal, locally_propertyIsLocal
StableUnderCompositionWithLocalizationAway 📖	MathDef	3 math math: isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway, isStandardSmooth_stableUnderCompositionWithLocalizationAway, StableUnderComposition.stableUnderCompositionWithLocalizationAway
StableUnderCompositionWithLocalizationAwaySource 📖	MathDef	2 math math: locally_stableUnderCompositionWithLocalizationAwaySource, locally_StableUnderCompositionWithLocalizationAwaySource
StableUnderCompositionWithLocalizationAwayTarget 📖	MathDef	4 math math: PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget, locally_stableUnderCompositionWithLocalizationAwayTarget, locally_StableUnderCompositionWithLocalizationAwayTarget, StableUnderCompositionWithLocalizationAwayTarget.and

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofLocalizationSpanTarget_iff_finite 📖	mathematical	—	OfLocalizationSpanTarget OfLocalizationFiniteSpanTarget	—	Ideal.span_eq_top_iff_finite Subtype.prop
ofLocalizationSpan_iff_finite 📖	mathematical	—	OfLocalizationSpan OfLocalizationFiniteSpan	—	Ideal.span_eq_top_iff_finite Subtype.prop

RingHom.HoldsForLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
holdsForLocalizationAway 📖	mathematical	RingHom.HoldsForLocalization	RingHom.HoldsForLocalizationAway	—	—
isLocalizationMap 📖	mathematical	RingHom.StableUnderComposition RingHom.LocalizationPreserves RingHom.HoldsForLocalization Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	IsLocalization.map CommRing.toCommSemiring	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.right Localization.isLocalization IsLocalization.localization_isScalarTower_of_submonoid_le IsLocalization.isLocalization_of_submonoid_le Submonoid.le_comap_map IsLocalization.ringHom_ext RingHom.ext IsLocalization.map_comp IsLocalization.map_eq
localRingHom 📖	mathematical	RingHom.StableUnderComposition RingHom.LocalizationPreserves RingHom.HoldsForLocalization Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass	Localization.AtPrime CommRing.toCommSemiring OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Localization.localRingHom	—	RingHom.instRingHomClass isLocalizationMap
mk 📖	mathematical	RingHom.RespectsIso Localization CommRing.toCommMonoid OreLocalization.instCommRing OreLocalization.oreSetComm algebraMap CommRing.toCommSemiring OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.instAlgebra Algebra.id	RingHom.HoldsForLocalization	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Localization.isLocalization AlgHom.comp_algebraMap

RingHom.HoldsForLocalizationAway

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
containsIdentities 📖	mathematical	RingHom.HoldsForLocalizationAway	RingHom.ContainsIdentities	—	of_bijective Function.bijective_id
of_bijective 📖	—	RingHom.HoldsForLocalizationAway Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	—	IsLocalization.at_units Submonoid.powers_one IsLocalization.isLocalization_of_algEquiv

RingHom.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_map 📖	mathematical	RingHom.IsStableUnderBaseChange	IsLocalization.map CommRing.toCommSemiring Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map IsScalarTower.of_algebraMap_eq' of_isLocalization IsLocalization.map_comp
localizationPreserves 📖	mathematical	RingHom.IsStableUnderBaseChange	RingHom.LocalizationPreserves	—	isLocalization_map
of_isLocalization 📖	mathematical	RingHom.IsStableUnderBaseChange algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	Algebra.isPushout_of_isLocalization

RingHom.LocalizationAwayPreserves

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	mathematical	RingHom.LocalizationAwayPreserves	RingHom.LocalizationAwayPreserves	—	—
respectsIso 📖	mathematical	RingHom.LocalizationAwayPreserves	RingHom.RespectsIso	—	IsLocalization.away_of_isUnit_of_bijective isUnit_one Equiv.bijective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingEquiv.bijective IsLocalization.Away.map.eq_1 IsLocalization.map_comp RingHom.comp_assoc RingEquiv.symm_comp RingHomCompTriple.comp_eq RingHomCompTriple.ids

RingHom.LocalizationPreserves

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
away 📖	mathematical	RingHom.LocalizationPreserves	RingHom.LocalizationAwayPreserves	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.map_powers

RingHom.OfLocalizationSpan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	mathematical	RingHom.OfLocalizationSpan	RingHom.OfLocalizationSpan	—	—
mk 📖	mathematical	RingHom.RespectsIso algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	RingHom.OfLocalizationSpan	—	IsScalarTower.right Algebra.to_smulCommClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Localization.isLocalization IsLocalization.ringHom_ext RingHom.ext RingHomCompTriple.comp_apply RingHomCompTriple.right_ids Algebra.TensorProduct.tmul_one_eq_one_tmul MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_eq AlgEquiv.commutes
ofIsLocalization 📖	—	RingHom.OfLocalizationSpan RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CommRing Algebra IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike RingHom.comp algebraMap	—	—	Localization.isLocalization IsLocalization.ringHom_ext RingHom.ext RingHom.comp_apply IsLocalization.map_comp AlgEquiv.commutes
ofIsLocalization' 📖	—	RingHom.OfLocalizationSpan RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CommRing Algebra IsLocalization.Away Set Set.instMembership DFunLike.coe RingHom RingHom.instFunLike IsLocalization.Away.map	—	—	ofIsLocalization IsLocalization.map_comp

RingHom.OfLocalizationSpanTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	mathematical	RingHom.OfLocalizationSpanTarget	RingHom.OfLocalizationSpanTarget	—	—
ofIsLocalization 📖	—	RingHom.OfLocalizationSpanTarget RingHom.RespectsIso Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CommRing Algebra IsLocalization.Away Set Set.instMembership RingHom.comp algebraMap	—	—	RingHom.comp_assoc RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.toRingHom_eq_coe AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.toRingEquiv_eq_coe AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.toRingEquiv_toRingHom Localization.isLocalization le_rfl Localization.coe_algEquiv_symm IsLocalization.map_comp RingHom.comp_id
ofLocalizationSpan 📖	mathematical	RingHom.OfLocalizationSpanTarget RingHom.StableUnderCompositionWithLocalizationAwaySource	RingHom.OfLocalizationSpan	—	Ideal.map_top RingHom.instRingHomClass Ideal.map_span Localization.isLocalization IsLocalization.map_comp

RingHom.PropertyIsLocal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HoldsForLocalizationAway 📖	mathematical	RingHom.PropertyIsLocal RingHom.ContainsIdentities	RingHom.HoldsForLocalizationAway	—	RingHomCompTriple.comp_eq RingHomCompTriple.ids StableUnderCompositionWithLocalizationAwayTarget
StableUnderCompositionWithLocalizationAwayTarget 📖	mathematical	RingHom.PropertyIsLocal	RingHom.StableUnderCompositionWithLocalizationAwayTarget	—	—
and 📖	mathematical	RingHom.PropertyIsLocal	RingHom.PropertyIsLocal	—	RingHom.LocalizationAwayPreserves.and localizationAwayPreserves RingHom.OfLocalizationSpanTarget.and ofLocalizationSpanTarget RingHom.OfLocalizationSpan.and ofLocalizationSpan RingHom.StableUnderCompositionWithLocalizationAwayTarget.and StableUnderCompositionWithLocalizationAwayTarget
localizationAwayPreserves 📖	mathematical	RingHom.PropertyIsLocal	RingHom.LocalizationAwayPreserves	—	—
ofLocalizationSpan 📖	mathematical	RingHom.PropertyIsLocal	RingHom.OfLocalizationSpan	—	—
ofLocalizationSpanTarget 📖	mathematical	RingHom.PropertyIsLocal	RingHom.OfLocalizationSpanTarget	—	—
respectsIso 📖	mathematical	RingHom.PropertyIsLocal	RingHom.RespectsIso	—	RingHom.LocalizationAwayPreserves.respectsIso localizationAwayPreserves

RingHom.StableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stableUnderCompositionWithLocalizationAway 📖	mathematical	RingHom.StableUnderComposition RingHom.HoldsForLocalizationAway	RingHom.StableUnderCompositionWithLocalizationAway	—	—

RingHom.StableUnderCompositionWithLocalizationAway

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
respectsIso 📖	mathematical	RingHom.StableUnderCompositionWithLocalizationAway	RingHom.RespectsIso	—	IsLocalization.away_of_isUnit_of_bijective isUnit_one RingEquiv.bijective

RingHom.StableUnderCompositionWithLocalizationAwayTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and 📖	mathematical	RingHom.StableUnderCompositionWithLocalizationAwayTarget	RingHom.StableUnderCompositionWithLocalizationAwayTarget	—	—

(root)

Definitions

Name	Category	Theorems
LocalizationPreserves 📖	MathDef	1 math math: isReduced_localizationPreserves
OfLocalizationMaximal 📖	MathDef	2 math math: isIntegrallyClosed_ofLocalizationMaximal, isReduced_ofLocalizationMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_localization 📖	mathematical	DFunLike.coe RingHom Localization.AtPrime Ideal.IsMaximal.isPrime' Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id OreLocalization.instZero CommMonoid.toMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toMulAction	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Ideal.IsMaximal.isPrime' Module.eq_zero_of_localization_maximal instIsLocalizedModuleLinearMapOfIsLocalization Localization.isLocalization
ideal_eq_bot_of_localization 📖	mathematical	IsLocalization.coeSubmodule Localization.AtPrime Ideal.IsMaximal.isPrime' OreLocalization.instCommSemiring Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid OreLocalization.instAlgebra Algebra.id Bot.bot Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule.instBot	Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.IsMaximal.isPrime' bot_unique eq_zero_of_localization Eq.le
ideal_eq_bot_of_localization' 📖	mathematical	Ideal.map Localization.AtPrime Ideal.IsMaximal.isPrime' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.IsMaximal.isPrime' Ideal.eq_of_localization_maximal Ideal.map_bot RingHom.instRingHomClass

---

← Back to Index