oreSetComm 📖 | CompOp | 528 mathmath: PrimeSpectrum.mapPiLocalization_id, Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, IsLocalizedModule.iso_symm_apply', Module.Finite.instLocalizationLocalizedModule, DivisibleHull.archimedeanClassMk_mk_eq, RatFunc.mk_def_of_ne, Algebra.exists_unramified_of_isUnramifiedAt, RatFunc.ofFractionRing_mk', Localization.Away.mk_eq_monoidOf_mk', RatFunc.mk_coe_def, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, HasStandardEtaleSurjectionOn.isStandardEtale, ClassGroup.mk0_integralRep, MaximalSpectrum.mapPiLocalization_bijective, Localization.algebraMap_injective_of_span_eq_top, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, ModuleCat.localizedModule_functor_map_exact, Localization.epi', FractionalIdeal.isPrincipal_of_isPrincipal_num, Algebra.GrothendieckGroup.instFG, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, Ideal.exists_mem_span_singleton_map_residueField_eq, Localization.mk_eq_monoidOf_mk', HomogeneousLocalization.val_nsmul, FractionRing.instIsScalarTower, Ideal.ker_algebraMap_residueField, ClassGroup.Quot_mk_eq_mk, LocalizedModule.restrictScalars_map_eq, Polynomial.fiberEquivQuotient_tmul, Localization.AtPrime.mapPiEvalRingHom_bijective, Module.rankAtStalk_eq, IsDedekindRing.toIsIntegralClosure, Module.Flat.localizedModule, Localization.instIsMulTorsionFree, WittVector.IsocrystalHom.frob_equivariant, instLiesOverFiberOfIsPrime, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Localization.mk_eq_mk', MaximalSpectrum.toPiLocalization_apply_apply, Localization.algEquiv_apply, Module.freeLocus_localization, Module.FinitePresentation.exists_notMem_bijective, Localization.algEquiv_mk', Localization.localRingHom_mk', Algebra.basicOpen_subset_etaleLocus_iff_etale, instIsAlgebraicResidueFieldOfIsIntegral, Localization.mulEquivOfQuotient_symm_monoidOf, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, RatFunc.mk_smul, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, AlgebraicGeometry.Scheme.basic_open_isOpenImmersion, LocalizedModule.mk_add_mk, Ideal.algebraMap_quotient_residueField_mk, Localization.liftOn_zero, IsLocalizedModule.iso_symm_apply, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, HomogeneousLocalization.range_awayMapAux_subset, instIsScalarTowerAtPrimeFractionRing_1, instIsFractionRingAtPrimeFractionRing, Algebra.QuasiFinite.instResidueField, Module.basicOpen_subset_freeLocus_iff, Localization.localRingHom_to_map, IsLocalizedModule.iso_apply_mk, LocalizedModule.divBy_apply, LocalizedModule.lift'_smul, DivisibleHull.mk_add_mk_left, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Algebra.basicOpen_subset_unramifiedLocus_iff, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Localization.localRingHom_injective_of_primesOver_eq_singleton, Localization.mk_algebraMap, Algebra.WeaklyQuasiFiniteAt.finite_residueField, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.AtPrime.isLocalRing, IsLocalization.instIsNoetherianRingLocalization, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, instFinitePresentationAway, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, FractionalIdeal.isUnit_num, LocalizedModule.divBy_mul_by, AlgebraicGeometry.Scheme.instIsOpenImmersionMapOfHomAwayAlgebraMap, instIsLocalHomAtPrimeRingHomAlgebraMap, LocalizedModule.map_surjective, HomogeneousLocalization.val_zero, FractionRing.algebraMap_liftAlgebra, FractionRing.isSeparable_of_isLocalization, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, MaximalSpectrum.mapPiLocalization_naturality, AlgebraicGeometry.stalkwise_SpecMap_iff, ModuleCat.instAdditiveLocalizationLocalizedModule_functor, HomogeneousLocalization.val_one, Algebra.FormallyEtale.instLocalization, instIsPushoutFractionRingPolynomial_1, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, LocalizedModule.mem_ker_mkLinearMap_iff, instEssFiniteTypeResidueField_1, Localization.algHom_ext_iff, Localization.AtPrime.isDedekindDomain, IsLocalizedModule.fromLocalizedModule.bij, Localization.isOrderedCancelMonoid, LocalizedModule.equivTensorProduct_symm_apply_tmul_one, LocalizedModule.equivTensorProduct_apply_mk, HomogeneousLocalization.val_smul, Localization.toLocalizationMap_eq_monoidOf, AlgebraicGeometry.StructureSheaf.comap_apply, LocalizedModule.map_injective, HomogeneousLocalization.val_pow, coeSubmodule_differentIdeal_fractionRing, Ideal.Fiber.lift_residueField_surjective, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, LocalizedModule.equivTensorProduct_symm_apply_tmul, RatFunc.mk_def, Module.FinitePresentation.linearEquivMap_symm_apply, RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, PrimeSpectrum.mapPiLocalization_bijective, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Algebra.algebraMap_intNorm_fractionRing, HomogeneousLocalization.val_zsmul, Localization.mk_intCast, Localization.epi, Ideal.algebraMap_residueField_surjective, FractionRing.instIsScalarTower_1, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, IsLocalizedModule.iso_symm_comp, HomogeneousLocalization.val_awayMap, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, Localization.awayMap_surjective_iff, Localization.liftOn₂_mk', IsLocalization.instIsScalarTowerLocalizationAtPrime, IsFractionRing.instAtPrimeFractionRing, Ideal.ResidueField.ringHom_ext_iff, RatFunc.ofFractionRing_one, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Algebra.GrothendieckGroup.lift_symm_apply, IsLocalizedModule.fromLocalizedModule.inj, instIsSeparableResidueFieldOfQuotientIdeal, Localization.mk_one_eq_monoidOf_mk, Algebra.basicOpen_subset_smoothLocus_iff_smooth, PrimeSpectrum.mapPiLocalization_comp, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Ideal.surjectiveOnStalks_residueField, ModuleCat.localizedModule_isLocalizedModule, Localization.algEquiv_mk, isIntegral_localization', RatFunc.smul_eq_C_mul, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor, Localization.mkHom_surjective, AlgebraicGeometry.Spec_map_localization_isIso, Algebra.WeaklyQuasiFiniteAt.finite_locoalization, RatFunc.ofFractionRing_zero, PrimeSpectrum.mem_image_comap_basicOpen, AlgebraicIndependent.lift_reprField, RatFunc.ofFractionRing_add, WittVector.IsocrystalEquiv.frob_equivariant, AlgHom.IsArithFrobAt.localize_algebraMap, Ideal.ResidueField.liftₐ_comp_toAlgHom, Localization.mulEquivOfQuotient_mk, DivisibleHull.instIsStrictOrderedModuleNNRat, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Localization.mk_eq_mk'_apply, Localization.mk_sum, Localization.localRingHom_id, instIsScalarTowerAtPrimeFractionRing, LocalizedModule.coe_map_eq, HomogeneousLocalization.val_sub, ModuleCat.localizedModule_functor_map, instIsAlgebraicQuotientIdealResidueField, Localization.mapPiEvalRingHom_bijective, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, Localization.mk_eq_monoidOf_mk'_apply, LocalizedModule.subsingleton_iff_ker_eq_top, Module.FinitePresentation.exists_free_localizedModule_powers, Algebra.QuasiFinite.finite_fiber, Algebra.QuasiFinite.instFiniteResidueField, IsLocalizedModule.fromLocalizedModule_mk, MaximalSpectrum.mapPiLocalization_id, Localization.instNoZeroDivisors, PrimeSpectrum.mapPiLocalization_naturality, Module.rankAtStalk_eq_finrank_tensorProduct, RatFunc.ofFractionRing_comp_algebraMap, Ideal.ResidueField.map_algebraMap, algebraMap_mk, ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, Ideal.ResidueField.exists_smul_eq_tmul_one, map_equiv_traceDual, HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization, Localization.AtPrime.comap_maximalIdeal, FractionRing.instIsFractionRing, Module.FinitePresentation.linearEquivMap_apply, Algebra.isUnramifiedAt_iff_map_eq, Ideal.relNorm_algebraMap', RatFunc.smul_eq_C_smul, Localization.finite_of_primesOver_eq_singleton, Localization.localAlgHom_apply, Localization.mulEquivOfQuotient_mk', PrimeSpectrum.toPiLocalization_bijective, HomogeneousLocalization.val_mul, PrimeSpectrum.residueField_comap, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, instFinitePresentationLocalizationLocalizedModule, IsLocalizedModule.lift_comp_iso, RatFunc.instIsScalarTowerOfIsDomainOfPolynomial, HomogeneousLocalization.val_add, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Localization.mkAddMonoidHom_apply, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, DivisibleHull.coeAddMonoidHom_apply, LocalizedModule.smul'_mk, DivisibleHull.instIsOrderedCancelAddMonoid, Localization.algEquiv_symm_mk', RatFunc.liftRingHom_ofFractionRing_algebraMap, localizedModuleIsLocalizedModule, HomogeneousLocalization.val_intCast, RatFunc.one_def, IsLocalization.isDomain_localization, RatFunc.div_smul, Algebra.basicOpen_subset_etaleLocus_iff, HomogeneousLocalization.val_natCast, RatFunc.inv_def, Ideal.relNorm_algebraMap, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, WittVector.inv_pair₂, instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient, instIsTopologicalRingLocalization, LocalizedModule.mk_neg, RatFunc.faithfulSMul, Localization.algEquiv_symm_mk, WittVector.exists_frobenius_solution_fractionRing, RingHom.surjective_localRingHom_of_surjective, RatFunc.instIsScalarTowerPolynomial, Localization.fg, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, IsGaloisGroup.toFractionRing, Localization.mk_one_eq_algebraMap, LocalizedModule.lift_comp, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, Algebra.IsSmoothAt.exists_notMem_smooth, Localization.mulEquivOfQuotient_symm_mk, Algebra.instEssFiniteTypeLocalization, WittVector.inv_pair₁, DivisibleHull.qsmul_def, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, Localization.mk_natCast, instLiesOverResidueFieldBotIdeal, Localization.mk_list_sum, Localization.monoidOf_eq_algebraMap, RatFunc.zero_def, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower_1, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap, PrimeSpectrum.piLocalizationToMaximal_surjective, IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, RingHom.HoldsForLocalization.localRingHom, Algebra.IsEtaleAt.exists_isStandardEtale, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, Localization.mk_self, IsLocalizedModule.fromLocalizedModule'_add, instFlatAtPrime, RatFunc.ofFractionRing_sub, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', AlgebraicIndependent.liftAlgHom_comp_reprField, DivisibleHull.qsmul_of_nonneg, RatFunc.ofFractionRing_neg, DivisibleHull.coeOrderAddMonoidHom_apply, AlgebraicGeometry.structureSheafInType.add_apply, Module.FinitePresentation.linearEquivMapExtendScalars_apply, IsLocalizedModule.iso_symm_apply_aux, DivisibleHull.nsmul_mk, ClassGroup.mk_eq_mk, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, Localization.isLocalization, instIsReducedLocalization, instFiniteTypeAway, IsArtinianRing.instLocalization, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.stalkwise_Spec_map_iff, ClassGroup.equivPic_symm_apply, LocalizedModule.lift_mk, RatFunc.instIsScalarTowerOfPolynomial, Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instEssFiniteTypeResidueField, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, IsLocalizedModule.map_bijective_iff_localizedModuleMap_bijective, Ideal.ResidueField.algHom_ext_iff, LocalizedModule.mul_by_divBy, Algebra.exists_formallyUnramified_of_isUnramifiedAt, localization_unit_isIso, Localization.mk_prod, HomogeneousLocalization.isUnit_iff_isUnit_val, Ideal.ResidueField.lift_algebraMap, WittVector.StandardOneDimIsocrystal.frobenius_apply, WeierstrassCurve.Affine.Point.toClass_some, LocalizedModule.map_exact, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, Algebra.FormallySmooth.instLocalization, MaximalSpectrum.mapPiLocalization_comp, HomogeneousLocalization.val_awayMap_eq_aux, Localization.mk_one, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app, IsLocalization.instIsScalarTowerAtPrimeFractionRing, isNilpotent_tensor_residueField_iff, Localization.AtPrime.instIsScalarTower_1, Algebra.weaklyQuasiFiniteAt_iff, Localization.AtPrime.instIsScalarTower, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, LocalizedModule.map_id, LocalizedModule.instIsScalarTower, HomogeneousLocalization.awayMapAux_mk, Module.mem_support_iff_nontrivial_residueField_tensorProduct, Localization.smul_mk, IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.coe_algEquiv, DivisibleHull.mk_add_mk, AlgHom.IsArithFrobAt.isArithFrobAt_localize, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, Localization.mk_pow, RatFunc.mk_def_of_mem, Localization.mulEquivOfQuotient_monoidOf, AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk, LocalizedModule.algebraMap_mk, instFiniteResidueField, DivisibleHull.archimedeanClassOrderIso_apply, Localization.mulEquivOfQuotient_apply, Algebra.exists_etale_of_isEtaleAt, AlgebraicIndependent.aevalEquivField_apply_coe, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.isIso_SpecMap_stakMap_localization, HomogeneousLocalization.val_neg, Surreal.dyadicMap_apply, Ideal.injective_algebraMap_quotient_residueField, HomogeneousLocalization.Away.eventually_smul_mem, Localization.add_mk, IsFractionRing.charP, Algebra.IsAlgebraic.rank_fractionRing, instIsPushoutFractionRingPolynomial, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, RatFunc.ofFractionRing_inv, LocalizedModule.lift_mk_one, Module.Invertible.instLocalizationLocalizedModule, RingHom.Flat.localRingHom, IsLocalizedModule.mk_eq_mk', IsLocalizedModule.map_injective_iff_localizedModuleMap_injective, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors, ModuleCat.localizedModuleMap_hom_apply, instIsScalarTowerQuotientIdealResidueField, DivisibleHull.zsmul_mk, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, Localization.mkHom_apply, RatFunc.neg_def, RatFunc.ofFractionRing_eq, DivisibleHull.neg_mk, MaximalSpectrum.toPiLocalization_injective, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, RatFunc.mk_zero, ModuleCat.localizedModule_functor_obj, DivisibleHull.qsmul_of_nonpos, AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_f, HomogeneousLocalization.den_smul_val, IsLocalization.instCompatibleSMulLocalizationOfIsScalarTower, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, RingHom.SurjectiveOnStalks.localRingHom_surjective, LocalizedModule.mk_smul_mk, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, WittVector.exists_frobenius_solution_fractionRing_aux, DivisibleHull.archimedeanClassOrderIso_symm_apply, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Localization.neg_mk, Localization.localRingHom_bijective_of_saturated_inf_eq_top, Localization.mk_mul, ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor, Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, Localization.mk_multiset_sum, MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, RingHom.RespectsIso.isLocalization_away_iff, RatFunc.mk_one', Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, DivisibleHull.instIsStrictOrderedModuleRat, Localization.awayMap_injective_iff, LocalizedModule.smul_eq_iff_of_mem, DivisibleHull.coe_add, RatFunc.isScalarTower_liftAlgebra, IsLocalization.isLocalization_atPrime_localization_atPrime, exists_bijective_map_powers, IsLocalizedModule.iso_localizedModule_eq_refl, FractionRing.isScalarTower_liftAlgebra, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, Localization.localRingHom_comp, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, LocalizedModule.map_mk, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, Localization.isLocalHom_localRingHom, instIsScalarTowerLocalizationAlgebraMapSubmonoid, PrimeSpectrum.piLocalizationToMaximal_bijective, RatFunc.sub_def, RatFunc.div_def, PrimeSpectrum.toPiLocalization_injective, RatFunc.add_def, RingHom.locally_iff_finite, DivisibleHull.mk_zero, DivisibleHull.zero_qsmul, IsLocalizedModule.fromLocalizedModule.surj, IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul, Localization.localRingHom_bijective_of_not_conductor_le, Algebra.algebraMap_intTrace_fractionRing, oreSetComm_oreDenom, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, Localization.r_iff_oreEqv_r, localization_unit_isIso', Submonoid.LocalizationMap.instIsCancelMulLocalization, Algebra.GrothendieckGroup.lift_apply, instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Localization.flat, RatFunc.toFractionRingRingEquiv_symm_eq, MvRatFunc.rank_eq_max_lift, IsLocalization.ideal_eq_iInf_comap_map_away, Polynomial.residueFieldMapCAlgEquiv_symm_X, Module.mem_freeLocus, Localization.liftOn_mk', Algebra.isSeparable_residueField_iff, ClassGroup.equivPic_apply, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, IsLocalizedModule.map_iso_commute, RatFunc.toFractionRingRingEquiv_apply, Ideal.algebraMap_residueField_eq_zero, Algebra.GrothendieckGroup.of_injective, LocalizedModule.zero_mk, Ideal.bijective_algebraMap_quotient_residueField, Ideal.absNorm_algebraMap, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Ideal.ResidueField.liftₐ_algebraMap, Localization.mk_self_mk, Localization.mulEquivOfQuotient_symm_mk', FractionRing.instFaithfulSMul, LocalizedModule.lift'_add, Algebra.basicOpen_subset_smoothLocus_iff, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, Algebra.QuasiFinite.instIsArtinianRingFiber, Localization.awayLift_mk, instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation, PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology, RatFunc.mul_def, RingHom.surjectiveOnStalks_iff_forall_maximal, ClassGroup.integralRep_mem_nonZeroDivisors, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, oreSetComm_oreNum, AlgebraicGeometry.structureSheafInType.smul_apply, Localization.mk_zero, AlgebraicGeometry.localRingHom_comp_stalkIso, Localization.AtPrime.map_eq_maximalIdeal, IsLocalizedModule.map_LocalizedModules, instFiniteDimensionalFractionRingOfFinite, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Surreal.dyadicMap_apply_pow, RatFunc.toFractionRingAlgEquiv_apply, Algebra.IsAlgebraic.rank_fractionRing_polynomial, ClassGroup.mk_def, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalizedModule.lift_iso, Ideal.Fiber.exists_smul_eq_one_tmul, FractionRing.mk_eq_div, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, Ideal.ResidueField.mapₐ_apply, LocalizedModule.mkLinearMap_apply, Localization.sub_mk, HomogeneousLocalization.algebraMap_apply, WeierstrassCurve.Affine.Point.toClass_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, Algebra.Etale.instAway, PrimeSpectrum.nontrivial_iff_mem_rangeComap, Module.FinitePresentation.exists_basis_localizedModule_powers, DivisibleHull.nnqsmul_mk, IsLocalization.isDomain_of_local_atPrime, Localization.add_mk_self, Polynomial.instEtaleUniversalCoprimeFactorizationRing, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, Polynomial.residueFieldMapCAlgEquiv_symm_C, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, LocalizedModule.oreEqv_eq_r, IsLocalizedModule.fromLocalizedModule'_smul, RingHom.surjective_localRingHom_iff, Algebra.QuasiFinite.instLocalization, instIsPushoutFractionRingMvPolynomial_1, RatFunc.ofFractionRing_algebraMap, Algebra.FormallyUnramified.instLocalization, Algebra.instIsStandardOpenImmersionAway, instIsFractionRingQuotientIdealResidueField, IsFractionRing.charZero, IsLocalizedModule.iso_mk_one, Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply, Localization.coe_algEquiv_symm, instIsPushoutFractionRingMvPolynomial, RatFunc.ofFractionRing_mul, Localization.algEquiv_symm_apply, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective, RatFunc.toFractionRing_eq
|