Basic

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

Statistics

Metric	Count
Definitions algEquiv, algEquivOfAlgEquiv, atUnits, liftAlgHom, unique, algEquiv, mapPiEvalRingHom, instAlgebraLocalizationAlgebraMapSubmonoid, localizationAlgebra	9
Theorems localization_map_bijective, localization_map_bijective, algEquivOfAlgEquiv_apply, algEquivOfAlgEquiv_eq, algEquivOfAlgEquiv_eq_map, algEquivOfAlgEquiv_mk', algEquivOfAlgEquiv_symm, algEquivOfAlgEquiv_symm_apply, algEquiv_apply, algEquiv_comp_algebraMap, algEquiv_comp_algebraMap_apply, algEquiv_mk', algEquiv_symm_apply, algEquiv_symm_mk', algHom_ext, algHom_subsingleton, algebraMap_apply_eq_map_map_submonoid, algebraMap_eq_map_map_submonoid, algebraMap_mk', bijective, coe_liftAlgHom, commutes, finite, iff_of_le_of_exists_dvd, instCompatibleSMulLocalizationOfIsScalarTower, isLocalization_iff_of_algEquiv, isLocalization_iff_of_isLocalization, isLocalization_iff_of_ringEquiv, isLocalization_of_algEquiv, liftAlgHom_apply, liftAlgHom_toRingHom, lift_algebraMap_eq_algebraMap, linearMap_compatibleSMul, map_injective_of_injective', map_units_map_submonoid, self, smul_mem_iff, algEquiv_apply, algEquiv_mk, algEquiv_mk', algEquiv_symm_apply, algEquiv_symm_mk, algEquiv_symm_mk', algHom_ext, algHom_ext_iff, coe_algEquiv, coe_algEquiv_symm, mapPiEvalRingHom_bijective, mk_intCast, mk_natCast, instIsLocalizationAlgebraMapSubmonoid, instIsScalarTowerLocalizationAlgebraMapSubmonoid, localizationAlgebraMap_def, localizationAlgebra_injective	54
Total	63

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localization_map_bijective 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSemifield SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing	Function.Bijective DFunLike.coe RingHom CommSemiring.toSemiring Semifield.toCommSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsField.localization_map_bijective toIsField

IsField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
localization_map_bijective 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsField	Function.Bijective DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	le_nonZeroDivisors_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain IsLocalization.injective IsLocalization.exists_mk'_eq mul_inv_cancel nonZeroDivisors.ne_zero DivisionRing.toNontrivial IsLocalization.eq_mk'_iff_mul_eq map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc mul_comm mul_one

IsLocalization

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	9 math math: algEquiv_symm_mk', algEquiv_apply, algEquiv_comp_algebraMap_apply, algEquiv_mk', algEquiv_comp_algebraMap, RatFunc.ofFractionRing_eq, algEquiv_symm_apply, RatFunc.toFractionRingRingEquiv_symm_eq, RatFunc.toFractionRing_eq
algEquivOfAlgEquiv 📖	CompOp	6 math math: algEquivOfAlgEquiv_eq, algEquivOfAlgEquiv_apply, algEquivOfAlgEquiv_mk', algEquivOfAlgEquiv_eq_map, algEquivOfAlgEquiv_symm_apply, algEquivOfAlgEquiv_symm
atUnits 📖	CompOp	—
liftAlgHom 📖	CompOp	3 math math: coe_liftAlgHom, liftAlgHom_apply, liftAlgHom_toRingHom
unique 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquivOfAlgEquiv_apply 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	DFunLike.coe algEquivOfAlgEquiv RingHom RingHom.instFunLike map RingHomClass.toRingHom AlgEquiv.toRingEquiv	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
algEquivOfAlgEquiv_eq 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	DFunLike.coe algEquivOfAlgEquiv RingHom RingHom.instFunLike algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_eq
algEquivOfAlgEquiv_eq_map 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	RingHomClass.toRingHom algEquivOfAlgEquiv map Submonoid.le_comap_of_map_le RingHom RingHom.instFunLike RingHom.instRingHomClass le_of_eq Submonoid PartialOrder.toPreorder Submonoid.instPartialOrder	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
algEquivOfAlgEquiv_mk' 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	DFunLike.coe algEquivOfAlgEquiv mk' Submonoid SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Set.mem_image_of_mem map_mk'
algEquivOfAlgEquiv_symm 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	AlgEquiv.symm algEquivOfAlgEquiv	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
algEquivOfAlgEquiv_symm_apply 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	DFunLike.coe AlgEquiv.symm algEquivOfAlgEquiv RingHom RingHom.instFunLike map RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm RingEquivClass.toRingEquiv AlgEquivClass.toRingEquivClass AlgEquiv.toRingEquiv	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
algEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CommSemiring.toSemiring AlgEquiv.instFunLike algEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map RingHom.id RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	—
algEquiv_comp_algebraMap 📖	mathematical	—	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass algEquiv algebraMap	—	ringHom_ext AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.ext AlgEquiv.commutes IsScalarTower.algebraMap_apply AlgEquiv.restrictScalars_apply
algEquiv_comp_algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.comp RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass algEquiv algebraMap	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass algEquiv_comp_algebraMap
algEquiv_mk' 📖	mathematical	—	DFunLike.coe AlgEquiv CommSemiring.toSemiring AlgEquiv.instFunLike algEquiv mk'	—	map_id_mk'
algEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CommSemiring.toSemiring AlgEquiv.instFunLike AlgEquiv.symm algEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map RingHom.id RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	—
algEquiv_symm_mk' 📖	mathematical	—	DFunLike.coe AlgEquiv CommSemiring.toSemiring AlgEquiv.instFunLike AlgEquiv.symm algEquiv mk'	—	map_id_mk'
algHom_ext 📖	—	AlgHom.comp CommSemiring.toSemiring Algebra.algHom	—	—	AlgHom.coe_ringHom_injective ringHom_ext AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext AlgHom.ext_iff
algHom_subsingleton 📖	mathematical	—	AlgHom CommSemiring.toSemiring	—	AlgHom.coe_ringHom_injective ringHom_ext AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap
algebraMap_apply_eq_map_map_submonoid 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap map Algebra.algebraMapSubmonoid	—	DFunLike.congr_fun MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map algebraMap_eq_map_map_submonoid
algebraMap_eq_map_map_submonoid 📖	mathematical	—	algebraMap CommSemiring.toSemiring map Algebra.algebraMapSubmonoid	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map map_unique IsScalarTower.algebraMap_apply
algebraMap_mk' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap mk' Algebra.algebraMapSubmonoid Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Algebra.mem_algebraMapSubmonoid_of_mem	—	Algebra.mem_algebraMapSubmonoid_of_mem eq_mk'_iff_mul_eq IsScalarTower.algebraMap_apply map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_comm mul_mk'_eq_mk'_of_mul mk'_mul_cancel_left
bijective 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring algebraMap	Function.Bijective DFunLike.coe RingHom RingHom.instFunLike	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Equiv.bijective ringHom_ext RingHom.ext AlgEquiv.commutes
coe_liftAlgHom 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe AlgHom AlgHom.funLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	liftAlgHom RingHom RingHom.instFunLike lift AlgHom.toRingHom	—	—
commutes 📖	mathematical	—	IsLocalization Algebra.algebraMapSubmonoid CommSemiring.toSemiring	—	IsScalarTower.algebraMap_apply IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_units surj map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul IsUnit.mul_val_inv map_one MonoidHomClass.toOneHomClass mul_one surj₂ exists_of_eq IsUnit.mul_right_cancel mul_assoc mul_comm
finite 📖	mathematical	—	Finite	—	exists_mk'_eq Finite.of_surjective Finite.instProd Subtype.finite
iff_of_le_of_exists_dvd 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder SetLike.instMembership Submonoid.instSetLike semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	IsLocalization	—	of_le_of_exists_dvd Localization.isLocalization isLocalization_iff_of_isLocalization
instCompatibleSMulLocalizationOfIsScalarTower 📖	mathematical	—	LinearMap.CompatibleSMul Localization CommSemiring.toCommMonoid CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul OreLocalization.instMonoid CommMonoid.toMonoid OreLocalization.oreSetComm Module.toDistribMulAction OreLocalization.instSemiring	—	IsScalarTower.right linearMap_compatibleSMul Localization.isLocalization
isLocalization_iff_of_algEquiv 📖	mathematical	—	IsLocalization	—	isLocalization_of_algEquiv
isLocalization_iff_of_isLocalization 📖	mathematical	—	IsLocalization	—	isLocalization_of_algEquiv
isLocalization_iff_of_ringEquiv 📖	mathematical	—	IsLocalization RingHom.toAlgebra RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring RingEquiv.toRingHom algebraMap	—	isLocalization_iff_of_algEquiv RingEquiv.map_mul' RingEquiv.map_add'
isLocalization_of_algEquiv 📖	mathematical	—	IsLocalization	—	AlgEquiv.commutes IsUnit.map MonoidHom.instMonoidHomClass map_units surj map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.apply_symm_apply Equiv.injective eq_iff_exists
liftAlgHom_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe AlgHom AlgHom.funLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	liftAlgHom RingHom RingHom.instFunLike lift AlgHom.toRingHom	—	—
liftAlgHom_toRingHom 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe AlgHom AlgHom.funLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	AlgHom.toRingHom liftAlgHom lift	—	—
lift_algebraMap_eq_algebraMap 📖	mathematical	—	lift algebraMap CommSemiring.toSemiring map_units_map_submonoid	—	lift_unique map_units_map_submonoid IsScalarTower.algebraMap_apply
linearMap_compatibleSMul 📖	mathematical	—	LinearMap.CompatibleSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	exists_mk'_eq IsUnit.smul_left_cancel map_units algebraMap_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_mk'_self map_smul
map_injective_of_injective' 📖	mathematical	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 SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe	map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass exists_mk'_eq map_mk' IsDomain.to_noZeroDivisors OneMemClass.one_mem SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass one_mul map_zero MonoidWithZeroHomClass.toZeroHomClass
map_units_map_submonoid 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	IsScalarTower.algebraMap_apply map_units Algebra.mem_algebraMapSubmonoid_of_mem
self 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder IsUnit.submonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	IsLocalization Algebra.id	—	isLocalization_of_algEquiv Localization.isLocalization
smul_mem_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Submodule.smul_mem_iff_of_isUnit map_units algebraMap_smul Submodule.smul_of_tower_mem Submonoid.isScalarTower

Localization

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	8 math math: algEquiv_apply, algEquiv_mk', algEquiv_mk, algEquiv_symm_mk', algEquiv_symm_mk, coe_algEquiv, coe_algEquiv_symm, algEquiv_symm_apply
mapPiEvalRingHom 📖	CompOp	1 math math: mapPiEvalRingHom_bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike algEquiv RingHom Semiring.toNonAssocSemiring OreLocalization.instCommSemiring RingHom.instFunLike IsLocalization.map isLocalization RingHom.id RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	—
algEquiv_mk 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike algEquiv IsLocalization.mk'	—	isLocalization mk_eq_mk' algEquiv_mk'
algEquiv_mk' 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike algEquiv IsLocalization.mk' OreLocalization.instCommSemiring isLocalization	—	IsLocalization.algEquiv_mk' isLocalization
algEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm algEquiv RingHom Semiring.toNonAssocSemiring OreLocalization.instCommSemiring RingHom.instFunLike IsLocalization.map isLocalization RingHom.id RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	—
algEquiv_symm_mk 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm algEquiv IsLocalization.mk'	—	isLocalization mk_eq_mk' algEquiv_symm_mk'
algEquiv_symm_mk' 📖	mathematical	—	DFunLike.coe AlgEquiv Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm algEquiv IsLocalization.mk' OreLocalization.instCommSemiring isLocalization	—	IsLocalization.algEquiv_symm_mk' isLocalization
algHom_ext 📖	—	AlgHom.comp Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.algHom Algebra.id OreLocalization.instIsScalarTower CommMonoid.toMonoid Monoid.toMulAction SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule IsScalarTower.right Algebra.toSMul	—	—	OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.algHom_ext isLocalization
algHom_ext_iff 📖	mathematical	—	AlgHom.comp Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.algHom Algebra.id OreLocalization.instIsScalarTower CommMonoid.toMonoid Monoid.toMulAction SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule IsScalarTower.right Algebra.toSMul	—	OreLocalization.instIsScalarTower IsScalarTower.right algHom_ext
coe_algEquiv 📖	mathematical	—	RingHomClass.toRingHom AlgEquiv Localization CommSemiring.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass algEquiv IsLocalization.map OreLocalization.instCommSemiring isLocalization RingHom.id le_rfl Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass PartialOrder.toPreorder Submonoid.instPartialOrder	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
coe_algEquiv_symm 📖	mathematical	—	RingHomClass.toRingHom AlgEquiv Localization CommSemiring.toCommMonoid CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra Algebra.id AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.symm algEquiv IsLocalization.map OreLocalization.instCommSemiring isLocalization RingHom.id le_rfl Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass PartialOrder.toPreorder Submonoid.instPartialOrder	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
mapPiEvalRingHom_bijective 📖	mathematical	—	Function.Bijective Localization Pi.commMonoid CommSemiring.toCommMonoid Submonoid.comap Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom Pi.nonAssocSemiring RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Pi.evalRingHom DFunLike.coe OreLocalization.instSemiring Pi.semiring OreLocalization.oreSetComm mapPiEvalRingHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isLocalization IsLocalization.exists_mk'_eq IsLocalization.eq IsLocalization.map_mk' Function.update_self eq_or_ne Function.update_of_ne MulZeroClass.zero_mul IsLocalization.mk'.congr_simp Subtype.coe_eta
mk_intCast 📖	mathematical	—	CommRing.toCommMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Localization OreLocalization.instRing OreLocalization.oreSetComm	—	eq_intCast RingHom.instRingHomClass mk_algebraMap
mk_natCast 📖	mathematical	—	CommSemiring.toCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Localization OreLocalization.instSemiring OreLocalization.oreSetComm	—	eq_natCast RingHom.instRingHomClass mk_algebraMap

(root)

Definitions

Name	Category	Theorems
instAlgebraLocalizationAlgebraMapSubmonoid 📖	CompOp	8 math math: instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerLocalizationAlgebraMapSubmonoid, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl
localizationAlgebra 📖	CompOp	2 math math: localizationAlgebraMap_def, localizationAlgebra_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizationAlgebraMapSubmonoid 📖	mathematical	—	IsLocalization Algebra.algebraMapSubmonoid CommSemiring.toSemiring Algebra.id	—	Algebra.algebraMapSubmonoid_self
instIsScalarTowerLocalizationAlgebraMapSubmonoid 📖	mathematical	—	IsScalarTower Localization CommSemiring.toCommMonoid Algebra.algebraMapSubmonoid CommSemiring.toSemiring OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Algebra.id IsScalarTower.right OreLocalization.instCommSemiring OreLocalization.instSemiring instAlgebraLocalizationAlgebraMapSubmonoid	—	IsScalarTower.of_algebraMap_eq Localization.isLocalization Submonoid.le_comap_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_eq
localizationAlgebraMap_def 📖	mathematical	—	algebraMap CommSemiring.toSemiring localizationAlgebra IsLocalization.map Algebra.algebraMapSubmonoid	—	—
localizationAlgebra_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	localizationAlgebra	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.map_injective_of_injective

---

← Back to Index