HomogeneousLocalization

📁 Source: Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Statistics

Metric	Count
Definitions HomogeneousLocalization, isLocalizationElem, mk, NumDenSameDeg, deg, den, embedding, instAdd, instCommMonoid, instMul, instNeg, instOne, instPowNat, instSMul, instZero, num, awayMap, awayMapₐ, deg, den, fromZeroRingHom, hasPow, homogeneousLocalizationAlgebra, homogeneousLocalizationCommRing, instAdd, instAlgebraSubtypeMemOfNat, instIntCast, instMul, instNatCast, instNeg, instOne, instSMul, instSMulInt, instSMulNat, instSub, instZero, map, mapId, mk, num, val	41
Theorems adjoin_mk_prod_pow_eq_top, eventually_smul_mem, finiteType, isLocalization_mul, mk_surjective, span_mk_prod_pow_eq_top, val_mk, deg_add, deg_mul, deg_neg, deg_one, deg_pow, deg_smul, deg_zero, den_add, den_mem, den_mul, den_neg, den_one, den_pow, den_smul, den_zero, ext, ext_iff, num_add, num_mul, num_neg, num_one, num_pow, num_smul, num_zero, algebraMap_apply, algebraMap_eq, awayMapAux_mk, awayMap_fromZeroRingHom, awayMap_mk, awayMapₐ_apply, den_mem, den_mem_deg, den_smul_val, eq_num_div_den, ext_iff_val, instIsScalarTowerSubtypeMemOfNatLocalization, instNontrivialAtPrime, isLocalRing, isUnit_iff_isUnit_val, map_mk, mk_add, mk_eq_zero_of_den, mk_eq_zero_of_num, mk_mul, mk_neg, mk_one, mk_pow, mk_smul, mk_surjective, mk_zero, num_mem_deg, one_eq, range_awayMapAux_subset, subsingleton, val_add, val_awayMap, val_awayMap_eq_aux, val_awayMap_mk, val_injective, val_injective_iff, val_intCast, val_mk, val_mul, val_natCast, val_neg, val_nsmul, val_one, val_pow, val_smul, val_sub, val_zero, val_zsmul, zero_eq	80
Total	121

HomogeneousLocalization

Definitions

Name	Category	Theorems
NumDenSameDeg 📖	CompData	31 math math: NumDenSameDeg.den_smul, mk_smul, mk_zero, NumDenSameDeg.den_add, NumDenSameDeg.num_mul, NumDenSameDeg.den_mul, NumDenSameDeg.deg_neg, NumDenSameDeg.deg_add, NumDenSameDeg.deg_one, mk_pow, mk_surjective, mk_one, zero_eq, mk_mul, NumDenSameDeg.deg_mul, NumDenSameDeg.num_pow, NumDenSameDeg.deg_zero, one_eq, NumDenSameDeg.num_one, mk_neg, NumDenSameDeg.num_neg, NumDenSameDeg.den_pow, NumDenSameDeg.den_neg, NumDenSameDeg.num_smul, NumDenSameDeg.den_one, NumDenSameDeg.num_zero, NumDenSameDeg.num_add, NumDenSameDeg.deg_pow, NumDenSameDeg.deg_smul, NumDenSameDeg.den_zero, mk_add
awayMap 📖	CompOp	22 math math: AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, awayMap_mk, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, val_awayMap, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, awayMapₐ_apply, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, awayMap_fromZeroRingHom, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, Away.isLocalization_mul, val_awayMap_eq_aux, val_awayMap_mk, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, AlgebraicGeometry.Proj.valuativeCriterion_existence_aux
awayMapₐ 📖	CompOp	2 math math: awayMapₐ_apply, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective
deg 📖	CompOp	2 math math: num_mem_deg, den_mem_deg
den 📖	CompOp	4 math math: eq_num_div_den, den_mem, den_smul_val, den_mem_deg
fromZeroRingHom 📖	CompOp	4 math math: awayMap_fromZeroRingHom, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, algebraMap_eq
hasPow 📖	CompOp	3 math math: AlgebraicGeometry.Proj.pow_apply, val_pow, mk_pow
homogeneousLocalizationAlgebra 📖	CompOp	3 math math: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', instIsScalarTowerSubtypeMemOfNatLocalization, algebraMap_apply
homogeneousLocalizationCommRing 📖	CompOp	82 math math: AlgebraicGeometry.Proj.awayMap_awayToSection_assoc, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, map_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.basicOpenIsoAway_hom, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, range_awayMapAux_subset, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app_assoc, Away.adjoin_mk_prod_pow_eq_top, AlgebraicGeometry.Proj.basicOpenToSpec_app_top, awayMap_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst, val_awayMap, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd, AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, awayMapₐ_apply, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, awayMap_fromZeroRingHom, instIsScalarTowerSubtypeMemOfNatLocalization, Away.span_mk_prod_pow_eq_top, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, AlgebraicGeometry.Proj.opensRange_awayι, algebraMap_eq, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec, Away.isLocalization_mul, isUnit_iff_isUnit_val, val_awayMap_eq_aux, val_awayMap_mk, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, awayMapAux_mk, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, isLocalRing, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun_asIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.Proj.instIsOpenImmersionAwayι, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toOpen_toSpec_val_c_app, Away.finiteType, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective, algebraMap_apply, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom
instAdd 📖	CompOp	6 math math: AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', val_add, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.Proj.stalkIso'_symm_mk, mk_add
instAlgebraSubtypeMemOfNat 📖	CompOp	7 math math: Away.adjoin_mk_prod_pow_eq_top, awayMapₐ_apply, instIsScalarTowerSubtypeMemOfNatLocalization, Away.span_mk_prod_pow_eq_top, algebraMap_eq, Away.finiteType, AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective
instIntCast 📖	CompOp	1 math math: val_intCast
instMul 📖	CompOp	6 math math: AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', mk_mul, val_mul, AlgebraicGeometry.Proj.stalkIso'_germ, AlgebraicGeometry.Proj.stalkIso'_symm_mk
instNatCast 📖	CompOp	1 math math: val_natCast
instNeg 📖	CompOp	3 math math: AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', mk_neg, val_neg
instOne 📖	CompOp	5 math math: AlgebraicGeometry.Proj.one_apply, val_one, mk_one, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', one_eq
instSMul 📖	CompOp	2 math math: mk_smul, val_smul
instSMulInt 📖	CompOp	1 math math: val_zsmul
instSMulNat 📖	CompOp	1 math math: val_nsmul
instSub 📖	CompOp	2 math math: AlgebraicGeometry.Proj.sub_apply, val_sub
instZero 📖	CompOp	7 math math: mk_zero, val_zero, mk_eq_zero_of_num, zero_eq, AlgebraicGeometry.Proj.zero_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', mk_eq_zero_of_den
map 📖	CompOp	1 math math: map_mk
mapId 📖	CompOp	5 math math: AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ
mk 📖	CompOp	—
num 📖	CompOp	3 math math: num_mem_deg, eq_num_div_den, den_smul_val
val 📖	CompOp	27 math math: AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, val_nsmul, eq_num_div_den, range_awayMapAux_subset, val_zero, val_one, val_injective, val_smul, val_pow, val_zsmul, val_awayMap, val_injective_iff, val_mk, val_sub, ext_iff_val, val_mul, val_add, val_intCast, val_natCast, isUnit_iff_isUnit_val, Away.val_mk, val_awayMap_eq_aux, val_awayMap_mk, val_neg, Away.eventually_smul_mem, den_smul_val, algebraMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom HomogeneousLocalization Localization CommRing.toCommMonoid Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring homogeneousLocalizationCommRing OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike algebraMap homogeneousLocalizationAlgebra val	—	AddSubgroupClass.toAddSubmonoidClass
algebraMap_eq 📖	mathematical	—	algebraMap SetLike.instMembership AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HomogeneousLocalization SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring homogeneousLocalizationCommRing instAlgebraSubtypeMemOfNat fromZeroRingHom	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid
awayMapAux_mk 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SetLike.instMembership Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingHom Away Localization.Away CommRing.toCommMonoid Semiring.toNonAssocSemiring homogeneousLocalizationCommRing Submonoid.powers OreLocalization.instSemiring Ring.toSemiring CommRing.toRing CommMonoid.toMonoid OreLocalization.oreSetComm RingHom.instFunLike Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.mem_powers_iff	—	AddSubgroupClass.toAddSubmonoidClass Submonoid.mem_powers_iff pow_one Algebra.smul_def IsScalarTower.right Localization.mk_self NumDenSameDeg.den_mem isUnit_iff_exists_inv instIsDedekindFiniteMonoid Submonoid.instSubmonoidClass Localization.mk_pow
awayMap_fromZeroRingHom 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom Away Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring homogeneousLocalizationCommRing Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike awayMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HomogeneousLocalization SetLike.GradeZero.instSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid fromZeroRingHom	—	AddSubgroupClass.toAddSubmonoidClass val_injective GradedRing.toGradedMonoid isUnit_of_dvd_unit map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IsLocalization.Away.algebraMap_isUnit Localization.isLocalization NumDenSameDeg.den_mem val_awayMap IsLocalization.lift_eq
awayMap_mk 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	DFunLike.coe RingHom Away Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring homogeneousLocalizationCommRing Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike awayMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow	—	AddSubgroupClass.toAddSubmonoidClass val_injective SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid
awayMapₐ_apply 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AlgHom AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Away SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring homogeneousLocalizationCommRing Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero instAlgebraSubtypeMemOfNat AlgHom.funLike awayMapₐ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike awayMap	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid
den_mem 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike den	—	NumDenSameDeg.den_mem
den_mem_deg 📖	mathematical	—	SetLike.instMembership deg den	—	—
den_smul_val 📖	mathematical	—	Localization CommRing.toCommMonoid OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right den val DFunLike.coe RingHom Semiring.toNonAssocSemiring OreLocalization.instSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra num	—	IsScalarTower.right den_mem eq_num_div_den Localization.isLocalization Localization.mk_eq_mk' IsLocalization.smul_mk' IsLocalization.mk'_mul_cancel_left
eq_num_div_den 📖	mathematical	—	val CommRing.toCommMonoid num Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike den den_mem	—	Quotient.out_eq'
ext_iff_val 📖	mathematical	—	val	—	val_injective
instIsScalarTowerSubtypeMemOfNatLocalization 📖	mathematical	—	IsScalarTower SetLike.instMembership AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid HomogeneousLocalization Localization CommRing.toCommMonoid Algebra.toSMul SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring homogeneousLocalizationCommRing instAlgebraSubtypeMemOfNat OreLocalization.instSemiring OreLocalization.oreSetComm homogeneousLocalizationAlgebra OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid Monoid.toMulAction SetLike.GradeZero.instAlgebraSubtypeMemOfNat IsScalarTower.right	—	AddSubgroupClass.toAddSubmonoidClass IsScalarTower.of_algebraMap_eq' GradedRing.toGradedMonoid
instNontrivialAtPrime 📖	mathematical	—	Nontrivial AtPrime	—	AddSubgroupClass.toAddSubmonoidClass val_zero val_one NeZero.one IsLocalRing.toNontrivial Localization.AtPrime.isLocalRing
isLocalRing 📖	mathematical	—	IsLocalRing AtPrime CommSemiring.toSemiring CommRing.toCommSemiring homogeneousLocalizationCommRing Ideal.primeCompl	—	AddSubgroupClass.toAddSubmonoidClass IsLocalRing.of_isUnit_or_isUnit_one_sub_self instNontrivialAtPrime val_sub val_one IsLocalRing.isUnit_or_isUnit_one_sub_self Localization.AtPrime.isLocalRing
isUnit_iff_isUnit_val 📖	mathematical	—	IsUnit Localization CommRing.toCommMonoid Ideal.primeCompl CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.instMonoid CommMonoid.toMonoid OreLocalization.oreSetComm val AtPrime MonoidWithZero.toMonoid Semiring.toMonoidWithZero homogeneousLocalizationCommRing	—	AddSubgroupClass.toAddSubmonoidClass mk_surjective Localization.isLocalization IsLocalization.exists_mk'_eq NumDenSameDeg.den_mem IsLocalization.eq_iff_exists one_mul IsLocalization.mk'_eq_iff_eq_mul IsLocalization.mk'_mul Localization.mk_eq_mk' MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Ideal.mul_mem_left Ideal.mul_mem_right Ideal.instIsTwoSided_1 IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid mk_mul ext_iff_val mul_comm val_one IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_mk 📖	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 DFunLike.coe	HomogeneousLocalization homogeneousLocalizationCommRing map NumDenSameDeg.deg NumDenSameDeg.num NumDenSameDeg.den NumDenSameDeg.den_mem	—	AddSubgroupClass.toAddSubmonoidClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
mk_add 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instAdd AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing HomogeneousLocalization instAdd	—	AddSubgroupClass.toAddSubmonoidClass
mk_eq_zero_of_den 📖	mathematical	NumDenSameDeg.den SetLike.instMembership NumDenSameDeg.deg ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	HomogeneousLocalization instZero	—	AddSubgroupClass.toAddSubmonoidClass AddSubmonoidClass.toZeroMemClass subsingleton NumDenSameDeg.den_mem
mk_eq_zero_of_num 📖	mathematical	NumDenSameDeg.num SetLike.instMembership NumDenSameDeg.deg ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	HomogeneousLocalization instZero	—	AddSubgroupClass.toAddSubmonoidClass AddSubmonoidClass.toZeroMemClass val_injective NumDenSameDeg.den_mem Localization.mk_zero val_zero
mk_mul 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instMul AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing HomogeneousLocalization instMul	—	AddSubgroupClass.toAddSubmonoidClass
mk_neg 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instNeg HomogeneousLocalization instNeg	—	—
mk_one 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instOne AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing HomogeneousLocalization instOne	—	AddSubgroupClass.toAddSubmonoidClass
mk_pow 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instPowNat AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing HomogeneousLocalization hasPow	—	AddSubgroupClass.toAddSubmonoidClass
mk_smul 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instSMul HomogeneousLocalization instSMul	—	—
mk_surjective 📖	mathematical	—	NumDenSameDeg HomogeneousLocalization	—	Quotient.mk''_surjective
mk_zero 📖	mathematical	—	NumDenSameDeg NumDenSameDeg.instZero AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing HomogeneousLocalization instZero	—	AddSubgroupClass.toAddSubmonoidClass
num_mem_deg 📖	mathematical	—	SetLike.instMembership deg num	—	—
one_eq 📖	mathematical	—	HomogeneousLocalization instOne Quotient.mk'' NumDenSameDeg Setoid.ker Localization CommRing.toCommMonoid NumDenSameDeg.embedding NumDenSameDeg.instOne AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	AddSubgroupClass.toAddSubmonoidClass
range_awayMapAux_subset 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Set Localization.Away CommRing.toCommMonoid Set.instHasSubset Set.range Away DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring homogeneousLocalizationCommRing Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero OreLocalization.instSemiring Ring.toSemiring CommRing.toRing CommMonoid.toMonoid OreLocalization.oreSetComm RingHom.instFunLike Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring HomogeneousLocalization val	—	AddSubgroupClass.toAddSubmonoidClass mk_surjective SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid SetLike.pow_mem_graded mul_pow NumDenSameDeg.den_mem Submonoid.mem_powers_iff
subsingleton 📖	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	HomogeneousLocalization	—	IsLocalization.subsingleton Localization.isLocalization Function.Injective.subsingleton val_injective
val_add 📖	mathematical	—	val HomogeneousLocalization instAdd Localization CommRing.toCommMonoid OreLocalization.instAdd CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule	—	AddSubgroupClass.toAddSubmonoidClass Quotient.ind₂' mk_add NumDenSameDeg.den_mem
val_awayMap 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	val Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Away Semiring.toNonAssocSemiring homogeneousLocalizationCommRing RingHom.instFunLike awayMap Localization.Away CommSemiring.toCommMonoid Localization CommRing.toCommMonoid OreLocalization.instSemiring CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instCommSemiring Localization.awayLift algebraMap OreLocalization.instAlgebra Algebra.id isUnit_of_dvd_unit OreLocalization.instCommMonoid map_dvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Monoid.toSemigroup NonUnitalRingHomClass.toMulHomClass NonAssocSemiring.toNonUnitalNonAssocSemiring RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Semigroup.toMul IsLocalization.Away.algebraMap_isUnit Localization.isLocalization	—	AddSubgroupClass.toAddSubmonoidClass isUnit_of_dvd_unit map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IsLocalization.Away.algebraMap_isUnit Localization.isLocalization val_awayMap_eq_aux
val_awayMap_eq_aux 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	val Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Away Semiring.toNonAssocSemiring homogeneousLocalizationCommRing RingHom.instFunLike awayMap Localization.Away CommRing.toCommMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing CommMonoid.toMonoid OreLocalization.oreSetComm Semigroup.toMul SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring	—	AddSubgroupClass.toAddSubmonoidClass Function.Injective.hasLeftInverse Zero.instNonempty val_injective range_awayMapAux_subset RingEquiv.apply_symm_apply
val_awayMap_mk 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	val Submonoid.powers DFunLike.coe RingHom Away Semiring.toNonAssocSemiring homogeneousLocalizationCommRing RingHom.instFunLike awayMap CommRing.toCommMonoid CommMonoid.toMonoid Submonoid Monoid.toMulOneClass Submonoid.instSetLike Submonoid.mem_powers_iff	—	AddSubgroupClass.toAddSubmonoidClass Submonoid.mem_powers_iff val_awayMap_eq_aux
val_injective 📖	mathematical	—	HomogeneousLocalization Localization CommRing.toCommMonoid val	—	Quotient.sound'
val_injective_iff 📖	mathematical	—	val	—	val_injective
val_intCast 📖	mathematical	—	val HomogeneousLocalization instIntCast Localization CommRing.toCommMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne OreLocalization.instRing CommRing.toRing OreLocalization.oreSetComm	—	AddSubgroupClass.toAddSubmonoidClass val_natCast Int.cast_natCast val_neg Nat.cast_add Nat.cast_one neg_add_rev Int.cast_negSucc
val_mk 📖	mathematical	—	val CommRing.toCommMonoid SetLike.instMembership NumDenSameDeg.deg NumDenSameDeg.num Submonoid Monoid.toMulOneClass CommMonoid.toMonoid Submonoid.instSetLike NumDenSameDeg.den NumDenSameDeg.den_mem	—	—
val_mul 📖	mathematical	—	val HomogeneousLocalization instMul Localization CommRing.toCommMonoid OreLocalization.instMul CommMonoid.toMonoid OreLocalization.oreSetComm	—	AddSubgroupClass.toAddSubmonoidClass Quotient.ind₂' mk_mul NumDenSameDeg.den_mem Localization.mk_mul
val_natCast 📖	mathematical	—	val HomogeneousLocalization instNatCast Localization CommRing.toCommMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne OreLocalization.instRing CommRing.toRing OreLocalization.oreSetComm	—	AddSubgroupClass.toAddSubmonoidClass val_zero Nat.cast_zero val_add val_one Nat.cast_add Nat.cast_one
val_neg 📖	mathematical	—	val HomogeneousLocalization instNeg Localization CommRing.toCommMonoid OreLocalization.instNegOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	Quotient.ind' mk_neg NumDenSameDeg.den_mem
val_nsmul 📖	mathematical	—	val HomogeneousLocalization instSMulNat Localization CommRing.toCommMonoid AddMonoid.toNatSMul OreLocalization.instAddMonoid CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule	—	val_smul AddCommMonoid.nat_isScalarTower OreLocalization.nsmul_eq_nsmul
val_one 📖	mathematical	—	val HomogeneousLocalization instOne Localization CommRing.toCommMonoid OreLocalization.instOne CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	AddSubgroupClass.toAddSubmonoidClass Localization.mk_one
val_pow 📖	mathematical	—	val HomogeneousLocalization hasPow Localization CommRing.toCommMonoid Monoid.toNatPow OreLocalization.instMonoid CommMonoid.toMonoid OreLocalization.oreSetComm	—	AddSubgroupClass.toAddSubmonoidClass Quotient.ind' mk_pow NumDenSameDeg.den_mem Submonoid.instSubmonoidClass Localization.mk_pow
val_smul 📖	mathematical	—	val HomogeneousLocalization instSMul Localization CommRing.toCommMonoid OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction	—	Quotient.ind' mk_smul NumDenSameDeg.den_mem NumDenSameDeg.num_smul
val_sub 📖	mathematical	—	val HomogeneousLocalization instSub Localization CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	AddSubgroupClass.toAddSubmonoidClass sub_eq_add_neg AddSubgroupClass.toNegMemClass val_neg val_add
val_zero 📖	mathematical	—	val HomogeneousLocalization instZero Localization CommRing.toCommMonoid OreLocalization.instZero CommMonoid.toMonoid OreLocalization.oreSetComm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toMulAction	—	AddSubgroupClass.toAddSubmonoidClass Localization.mk_zero NumDenSameDeg.den_mem
val_zsmul 📖	mathematical	—	val HomogeneousLocalization instSMulInt Localization CommRing.toCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	val_smul AddCommGroup.intIsScalarTower OreLocalization.zsmul_eq_zsmul
zero_eq 📖	mathematical	—	HomogeneousLocalization instZero Quotient.mk'' NumDenSameDeg Setoid.ker Localization CommRing.toCommMonoid NumDenSameDeg.embedding NumDenSameDeg.instZero AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	AddSubgroupClass.toAddSubmonoidClass

HomogeneousLocalization.Away

Definitions

Name	Category	Theorems
isLocalizationElem 📖	CompOp	2 math math: isLocalization_mul, AlgebraicGeometry.Proj.awayι_preimage_basicOpen
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_mk_prod_pow_eq_top 📖	mathematical	SetLike.instMembership Algebra.adjoin SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring SetLike.GradeZero.instAlgebraSubtypeMemOfNat Set.range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	HomogeneousLocalization.Away HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero HomogeneousLocalization.instAlgebraSubtypeMemOfNat setOf Finset.sum Finset.univ AddMonoid.toNatSMul Finset.prod CommRing.toCommMonoid Monoid.toNatPow SetLike.prod_pow_mem_graded AddCommMonoid.toAddMonoid Ring.toSemiring	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid SetLike.prod_pow_mem_graded top_le_iff Algebra.adjoin_le_iff Set.range_subset_iff algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass Algebra.subset_adjoin Algebra.adjoin_mono Finset.sum_congr dite_mul MulZeroClass.zero_mul Finset.sum_attach_eq_sum_dite dite_apply Nat.instCanonicallyOrderedAdd Finset.prod_congr pow_dite pow_zero Finset.prod_attach_eq_prod_dite
eventually_smul_mem 📖	mathematical	SetLike.instMembership	Filter.Eventually Localization CommRing.toCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id SetLike.coe AddMonoid.toNatSMul AddCommMonoid.toAddMonoid OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid Monoid.toMulAction Algebra.toSMul IsScalarTower.right Monoid.toNatPow HomogeneousLocalization.val Filter.atTop Nat.instPreorder	—	AddSubgroupClass.toAddSubmonoidClass IsScalarTower.right HomogeneousLocalization.den_mem Filter.mem_of_superset Filter.Ici_mem_atTop ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass pow_add MulZeroClass.mul_zero zero_smul SemigroupAction.mul_smul HomogeneousLocalization.den_smul_val Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass smul_eq_mul add_smul DirectSum.degree_eq_of_mem_mem SetLike.pow_mem_graded GradedRing.toGradedMonoid HomogeneousLocalization.den_mem_deg SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul HomogeneousLocalization.num_mem_deg
finiteType 📖	mathematical	SetLike.instMembership	Algebra.FiniteType HomogeneousLocalization.Away SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring Nat.instAddMonoid AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero HomogeneousLocalization.instAlgebraSubtypeMemOfNat	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero SetLike.prod_pow_mem_graded adjoin_mk_prod_pow_eq_top Subtype.range_coe_subtype nsmul_zero SetLike.GradedMonoid.toGradedOne Set.finite_singleton Algebra.adjoin_le_iff Finset.prod_congr pow_zero Finset.prod_const_one HomogeneousLocalization.val_injective pow_mem Submonoid.instSubmonoidClass pow_one HomogeneousLocalization.val_pow Localization.mk_pow one_pow SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass Algebra.self_mem_adjoin_singleton Finset.sum_congr Unique.instSubsingleton IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Set.Finite.subset Set.finite_range Subtype.finite Finite.instProd Finite.of_fintype Pi.finite mul_le_mul_iff_of_pos_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono smul_eq_mul Finset.sum_mul mul_comm Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_le_mul_left covariant_swap_mul_of_covariant_mul Nat.instMulLeftMono LE.le.trans_lt le_rfl Subtype.forall'
isLocalization_mul 📖	mathematical	SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsLocalization.Away HomogeneousLocalization.Away CommRing.toCommSemiring HomogeneousLocalization.homogeneousLocalizationCommRing Nat.instAddCommMonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring isLocalizationElem RingHom.toAlgebra HomogeneousLocalization.awayMap	—	AddSubgroupClass.toAddSubmonoidClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.algebraMap_toAlgebra SetLike.mul_mem_graded SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.nsmul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.smul_nat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.mul_one SetLike.pow_mem_graded IsUnit.pow isUnit_iff_exists_inv instIsDedekindFiniteMonoid HomogeneousLocalization.val_injective HomogeneousLocalization.val_mul Localization.mk_mul HomogeneousLocalization.val_one Localization.mk_one Localization.mk_eq_mk_iff Localization.r_iff_exists one_mul mul_one Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mk_surjective Submonoid.instSubmonoidClass HomogeneousLocalization.val_pow Localization.mk_pow Mathlib.Tactic.Ring.pow_one_cast
mk_surjective 📖	—	SetLike.instMembership	—	—	AddSubgroupClass.toAddSubmonoidClass HomogeneousLocalization.mk_surjective HomogeneousLocalization.subsingleton ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass HomogeneousLocalization.val_injective DirectSum.degree_eq_of_mem_mem SetLike.pow_mem_graded GradedRing.toGradedMonoid
span_mk_prod_pow_eq_top 📖	mathematical	SetLike.instMembership Algebra.adjoin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.GradeZero.instCommSemiring CommRing.toCommSemiring AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing GradedRing.toGradedMonoid CommSemiring.toSemiring SetLike.GradeZero.instAlgebraSubtypeMemOfNat Set.range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Submodule.span HomogeneousLocalization.Away SetLike.GradeZero.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HomogeneousLocalization.homogeneousLocalizationCommRing Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toModule HomogeneousLocalization.instAlgebraSubtypeMemOfNat setOf Finset.sum Finset.univ AddMonoid.toNatSMul Finset.prod CommRing.toCommMonoid Monoid.toNatPow SetLike.prod_pow_mem_graded Ring.toSemiring Submodule Submodule.instTop	—	AddSubgroupClass.toAddSubmonoidClass GradedRing.toGradedMonoid SetLike.prod_pow_mem_graded Unique.instSubsingleton top_le_iff HomogeneousLocalization.mk_surjective HomogeneousLocalization.subsingleton DirectSum.decompose_of_mem_same Algebra.adjoin_eq_span Submodule.span_induction Submonoid.exists_of_mem_closure_range Submodule.subset_span DirectSum.degree_eq_of_mem_mem SetLike.pow_mem_graded HomogeneousLocalization.val_injective HomogeneousLocalization.NumDenSameDeg.den_mem DirectSum.decompose_of_mem_ne Localization.mk_zero HomogeneousLocalization.val_zero ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass DirectSum.decompose_zero DirectSum.decompose_add HomogeneousLocalization.val_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submonoid.mul_mem one_mul Algebra.smul_def DirectSum.coe_decompose_mul_of_left_mem_zero HomogeneousLocalization.val_mul Localization.mk_mul Submodule.smul_mem
val_mk 📖	mathematical	SetLike.instMembership AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	HomogeneousLocalization.val Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Submonoid Monoid.toMulOneClass CommMonoid.toMonoid Submonoid.instSetLike Monoid.toNatPow	—	AddSubgroupClass.toAddSubmonoidClass

HomogeneousLocalization.NumDenSameDeg

Definitions

Name	Category	Theorems
deg 📖	CompOp	33 math math: den_smul, HomogeneousLocalization.map_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, den_add, num_mul, den_mul, deg_neg, deg_add, deg_one, HomogeneousLocalization.val_mk, deg_mul, num_pow, deg_zero, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, num_one, den_mem, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, num_neg, den_pow, den_neg, num_smul, ext_iff, AlgebraicGeometry.mem_basicOpen_den, den_one, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, num_zero, num_add, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, deg_pow, deg_smul, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, den_zero, AlgebraicGeometry.Proj.stalkIso'_symm_mk
den 📖	CompOp	14 math math: den_smul, HomogeneousLocalization.map_mk, den_add, den_mul, HomogeneousLocalization.val_mk, den_mem, den_pow, den_neg, ext_iff, AlgebraicGeometry.mem_basicOpen_den, den_one, num_add, den_zero, AlgebraicGeometry.Proj.stalkIso'_symm_mk
embedding 📖	CompOp	2 math math: HomogeneousLocalization.zero_eq, HomogeneousLocalization.one_eq
instAdd 📖	CompOp	4 math math: den_add, deg_add, num_add, HomogeneousLocalization.mk_add
instCommMonoid 📖	CompOp	—
instMul 📖	CompOp	4 math math: num_mul, den_mul, HomogeneousLocalization.mk_mul, deg_mul
instNeg 📖	CompOp	4 math math: deg_neg, HomogeneousLocalization.mk_neg, num_neg, den_neg
instOne 📖	CompOp	5 math math: deg_one, HomogeneousLocalization.mk_one, HomogeneousLocalization.one_eq, num_one, den_one
instPowNat 📖	CompOp	4 math math: HomogeneousLocalization.mk_pow, num_pow, den_pow, deg_pow
instSMul 📖	CompOp	4 math math: den_smul, HomogeneousLocalization.mk_smul, num_smul, deg_smul
instZero 📖	CompOp	5 math math: HomogeneousLocalization.mk_zero, HomogeneousLocalization.zero_eq, deg_zero, num_zero, den_zero
num 📖	CompOp	16 math math: HomogeneousLocalization.map_mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, num_mul, HomogeneousLocalization.val_mk, num_pow, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, num_one, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, num_neg, num_smul, ext_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, num_zero, num_add, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deg_add 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
deg_mul 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instMul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
deg_neg 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instNeg	—	—
deg_one 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
deg_pow 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instPowNat AddMonoid.toNatSMul AddCommMonoid.toAddMonoid	—	—
deg_smul 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instSMul	—	—
deg_zero 📖	mathematical	—	deg HomogeneousLocalization.NumDenSameDeg instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
den_add 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instAdd den Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
den_mem 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike deg den	—	—
den_mul 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instMul den Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
den_neg 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instNeg den	—	—
den_one 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instOne den AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
den_pow 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instPowNat den Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
den_smul 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instSMul den	—	—
den_zero 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instZero den AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
ext 📖	—	deg SetLike.instMembership num den	—	—	—
ext_iff 📖	mathematical	—	deg SetLike.instMembership num den	—	ext
num_add 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instAdd num Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul den	—	—
num_mul 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instMul num Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
num_neg 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instNeg num NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—
num_one 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instOne num AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
num_pow 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instPowNat num Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—
num_smul 📖	mathematical	—	SetLike.instMembership deg HomogeneousLocalization.NumDenSameDeg instSMul num	—	—
num_zero 📖	mathematical	—	num HomogeneousLocalization.NumDenSameDeg instZero SetLike.instMembership deg ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—

(root)

Definitions

Name	Category	Theorems
HomogeneousLocalization 📖	CompOp	47 math math: HomogeneousLocalization.subsingleton, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, HomogeneousLocalization.val_nsmul, HomogeneousLocalization.map_mk, HomogeneousLocalization.mk_smul, HomogeneousLocalization.mk_zero, HomogeneousLocalization.range_awayMapAux_subset, HomogeneousLocalization.val_zero, HomogeneousLocalization.val_one, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, HomogeneousLocalization.mk_eq_zero_of_num, HomogeneousLocalization.val_injective, HomogeneousLocalization.val_smul, HomogeneousLocalization.val_pow, HomogeneousLocalization.val_zsmul, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, HomogeneousLocalization.mk_pow, HomogeneousLocalization.val_sub, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, HomogeneousLocalization.mk_surjective, HomogeneousLocalization.mk_one, HomogeneousLocalization.awayMap_fromZeroRingHom, HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization, HomogeneousLocalization.zero_eq, HomogeneousLocalization.mk_mul, HomogeneousLocalization.val_mul, HomogeneousLocalization.val_add, HomogeneousLocalization.val_intCast, AlgebraicGeometry.Proj.awayι_toSpecZero, HomogeneousLocalization.val_natCast, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, AlgebraicGeometry.Proj.awayι_toSpecZero_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, HomogeneousLocalization.one_eq, HomogeneousLocalization.algebraMap_eq, HomogeneousLocalization.mk_neg, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.val_neg, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, HomogeneousLocalization.mk_eq_zero_of_den, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, HomogeneousLocalization.algebraMap_apply, HomogeneousLocalization.mk_add

---

← Back to Index