Defs

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

Statistics

Metric	Count
Definitions IsLocalization', fintype', invertible_mk'_one, map, mk', ringEquivOfRingEquiv, sec, toLocalizationMap, uniqueOfZeroMem, instUniqueLocalization, mkAddMonoidHom	11
Theorems toIsLocalizationMap, algebraMap_isUnit_iff, at_units, coe_toLocalizationMap, eq, eq_iff_eq, eq_iff_exists, eq_mk'_iff_mul_eq, eq_mk'_of_mul_eq, eq_of_eq, eq_zero_of_fst_eq_zero, exists_mk'_eq, exists_of_eq, ext, injective, injective_iff_isRegular, injective_iff_map_algebraMap_eq, injective_of_map_algebraMap_zero, injectiveₛ, invertible_mk'_one_invOf, isDomain_localization, isDomain_of_le_nonZeroDivisors, isLocalization_iff_of_base_ringEquiv, isLocalization_of_base_ringEquiv, isRegular_mk', isUnit_comp, lift_comp, lift_eq, lift_eq_iff, lift_id, lift_injective_iff, lift_mk', lift_mk'_spec, lift_of_comp, lift_spec_mul_add, lift_surjective_iff, lift_unique, map_comp, map_comp_map, map_eq, map_eq_zero_iff, map_id, map_id_mk', map_injective_of_injective, map_left_cancel, map_map, map_mk', map_nonZeroDivisors_le, map_right_cancel, map_smul, map_surjective_of_surjective, map_unique, map_units, mk'_add, mk'_add_eq_iff_add_mul_eq_mul, mk'_cancel, mk'_eq_iff_eq, mk'_eq_iff_eq', mk'_eq_iff_eq_mul, mk'_eq_iff_mk'_eq, mk'_eq_mul_mk'_one, mk'_eq_of_eq, mk'_eq_of_eq', mk'_eq_zero_iff, mk'_mul, mk'_mul_cancel_left, mk'_mul_cancel_right, mk'_mul_mk'_eq_one, mk'_mul_mk'_eq_one', mk'_neg, mk'_one, mk'_pow, mk'_sec, mk'_self, mk'_self', mk'_self'', mk'_spec, mk'_spec', mk'_spec'_mk, mk'_spec_mk, mk'_sub, mk'_surjective, mk'_zero, monoidHom_ext, mul_add_inv_left, mul_mk'_eq_mk'_of_mul, ne_zero_of_mk'_ne_zero, noZeroDivisors, nonZeroDivisors_le_comap, of_le, of_le_of_exists_dvd, ringEquivOfRingEquiv_apply, ringEquivOfRingEquiv_eq, ringEquivOfRingEquiv_eq_map, ringEquivOfRingEquiv_mk', ringEquivOfRingEquiv_symm, ringEquivOfRingEquiv_symm_apply, ringHom_ext, sec_fst_ne_zero, sec_snd_ne_zero, sec_spec, sec_spec', smul_bijective, smul_mk', smul_mk'_one, smul_mk'_self, subsingleton, subsingleton_iff, surj, surj₂, toLocalizationMap_apply, toLocalizationMap_sec, toLocalizationMap_toMonoidHom, to_map_eq_zero_iff, to_map_ne_zero_of_mem_nonZeroDivisors, add_mk, add_mk_self, instNoZeroDivisors, isLocalization, mkAddMonoidHom_apply, mk_algebraMap, mk_eq_mk', mk_eq_mk'_apply, mk_list_sum, mk_multiset_sum, mk_one_eq_algebraMap, mk_sum, monoidOf_eq_algebraMap, neg_mk, sub_mk, toLocalizationMap_eq_monoidOf, isLocalization_iff, isLocalization_iff_isLocalizationMap	133
Total	144

IsLocalization

Definitions

Name	Category	Theorems
fintype' 📖	CompOp	—
invertible_mk'_one 📖	CompOp	1 math math: invertible_mk'_one_invOf
map 📖	CompOp	46 math math: algebraMap_apply_eq_map_map_submonoid, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, map_surjective_of_surjective, map_mk', map_comp_map, isIntegral_localization, algEquiv_apply, Localization.algEquiv_apply, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, algEquivOfAlgEquiv_apply, ringEquivOfRingEquiv_symm_apply, map_injective_of_injective', map_map, isIntegral_localization', map_comp, map_eq, AlgHom.toKerIsLocalization_apply, map_unique, ringEquivOfRingEquiv_eq_map, FractionalIdeal.canonicalEquiv_spanSingleton, RingHom.toKerIsLocalization_apply, map_smul, algEquivOfAlgEquiv_eq_map, algEquivOfAlgEquiv_symm_apply, map_injective_of_injective, map_id, Localization.coe_algEquiv, ker_map, localizationAlgebraMap_def, RingHom.IsStableUnderBaseChange.isLocalization_map, RingHom.isIntegralElem_localization_at_leadingCoeff, mapₐ_coe, algEquiv_symm_apply, FractionalIdeal.mem_canonicalEquiv_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, RingHom.HoldsForLocalization.isLocalizationMap, ringEquivOfRingEquiv_apply, FractionalIdeal.mem_extended_iff, RingHom.toKerIsLocalization_isLocalizedModule, map_id_mk', is_integral_localization_at_leadingCoeff, FractionalIdeal.coe_extended_eq_span, Localization.coe_algEquiv_symm, algebraMap_eq_map_map_submonoid, Polynomial.isIntegral_isLocalization_polynomial_quotient, Localization.algEquiv_symm_apply
mk' 📖	CompOp	108 math math: RatFunc.mk_def_of_ne, RatFunc.ofFractionRing_mk', RatFunc.mk_coe_def, LaurentPolynomial.mk'_one_X_pow, selfZPow_of_nonpos, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, algEquiv_symm_mk', LaurentPolynomial.mk'_mul_T, mk'_spec_mk, AtPrime.mk'_mem_maximal_iff, Ring.ordFrac_eq_div, map_mk', mk'_surjective, selfZPow_pow_sub, mk'_eq_of_eq, Localization.mk_eq_mk', mk'_pow, mk'_tmul, LaurentPolynomial.mk'_one_X, Localization.algEquiv_mk', Localization.localRingHom_mk', lift_mk'_spec, mem_span_map, IsFractionRing.mk'_eq_one_iff_eq, IsFractionRing.mk'_eq_div, smul_mk'_self, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, mk'_mul_cancel_left, IsFractionRing.exists_reduced_fraction, isRegular_mk', smul_mk', RatFunc.mk_eq_mk', mk'_eq_mul_mk'_one, mk'_sub, AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, mk'_self, mk'_spec', mk'_mem_iff, Localization.algEquiv_mk, mk'_eq_algebraMap_mk'_of_submonoid_le, mk'_eq_mk', LaurentPolynomial.mk'_eq, Localization.mk_eq_mk'_apply, mk'_algebraMap_eq_mk', lift_mk', mk'_self'', selfZPow_of_neg, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', mk'_add_eq_iff_add_mul_eq_mul, mk'_mem_map_algebraMap_iff, algEquivOfAlgEquiv_mk', mk'_mul_mk'_eq_one', Localization.algEquiv_symm_mk', IsFractionRing.inv_def, mk'_self', IsFractionRing.mk'_num_den, Localization.algEquiv_symm_mk, mk'_eq_iff_eq, Valuation.extendToLocalization_mk', mem_invSubmonoid_iff_exists_mk', mk'_neg, mk'_sec, algEquiv_mk', mk'_eq_iff_eq_mul, IsFractionRing.mk'_mk_eq_div, mk'_eq_of_eq', mk'_eq_iff_mk'_eq, smul_mk'_one, IsLocalizedModule.mk'_smul_mk', mk'_cancel, IsFractionRing.mk'_eq_zero_iff_eq_zero, toInvSubmonoid_eq_mk', tmul_mk', mk'_zero, mk'_one, RatFunc.mk_def_of_mem, mk'_mul_mk'_eq_one, Surreal.dyadicMap_apply, mk'_eq_zero_iff, LocalizedModule.mk'_smul_mk, selfZPow_sub_natCast, MvPolynomial.isLocalization_C_mk', mk'_spec'_mk, AtPrime.isUnit_mk'_iff, mk'_mul_cancel_right, algebraMap_mk', mk'_eq_iff_eq', eq_mk'_of_mul_eq, selfZPow_neg_natCast, invertible_mk'_one_invOf, mul_mk'_eq_mk'_of_mul, eq_mk'_iff_mul_eq, mk'_add, AtPrime.equivQuotMaximalIdeal_symm_apply_mk, lift_eq_iff, LocalizedModule.algebraMap_mk', FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, eq, Surreal.dyadicMap_apply_pow, map_id_mk', mem_span_iff, IsFractionRing.lift_mk', mk'_spec, Localization.mem_range_mapToFractionRing_iff, exists_mk'_eq, mk'_mul, IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk', ringEquivOfRingEquiv_mk'
ringEquivOfRingEquiv 📖	CompOp	6 math math: ringEquivOfRingEquiv_symm_apply, ringEquivOfRingEquiv_eq_map, ringEquivOfRingEquiv_symm, ringEquivOfRingEquiv_eq, ringEquivOfRingEquiv_apply, ringEquivOfRingEquiv_mk'
sec 📖	CompOp	7 math math: sec_spec', IsFractionRing.inv_def, LocalizedModule.smul_def, mk'_sec, toLocalizationMap_sec, sec_spec, FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal
toLocalizationMap 📖	CompOp	6 math math: lift_spec_mul_add, Localization.toLocalizationMap_eq_monoidOf, toLocalizationMap_apply, coe_toLocalizationMap, toLocalizationMap_sec, toLocalizationMap_toMonoidHom
uniqueOfZeroMem 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_isUnit_iff 📖	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 semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	—	isUnit_iff_dvd_one surj eq_iff_exists map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass one_mul mul_assoc MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_left_comm isUnit_of_dvd_unit map_dvd map_units
at_units 📖	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	—	Subtype.prop mul_one
coe_toLocalizationMap 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommSemiring.toCommMonoid Submonoid.LocalizationMap.instFunLike toLocalizationMap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
eq 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.eq
eq_iff_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Submonoid.LocalizationMap.eq_iff_eq
eq_iff_exists 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.eq_iff_exists
eq_mk'_iff_mul_eq 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.eq_mk'_iff_mul_eq
eq_mk'_of_mul_eq 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	DFunLike.coe RingHom RingHom.instFunLike algebraMap mk'	—	eq_mk'_iff_mul_eq map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
eq_of_eq 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike algebraMap	—	—	Submonoid.LocalizationMap.eq_of_eq
eq_zero_of_fst_eq_zero 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	IsUnit.mul_left_eq_zero map_units RingHom.map_zero
exists_mk'_eq 📖	mathematical	—	mk'	—	mk'_surjective
exists_of_eq 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.exists_of_eq IsLocalization'.toIsLocalizationMap
ext 📖	—	AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring MulOne.toMul DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	—	monoidHom_ext MonoidHom.ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
injective 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	injectiveₛ isRegular_iff_mem_nonZeroDivisors
injective_iff_isRegular 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.injective_iff
injective_iff_map_algebraMap_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	isUnit_comp lift_of_comp lift_injective_iff
injective_of_map_algebraMap_zero 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	injective_iff_map_algebraMap_eq sub_eq_zero map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
injectiveₛ 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Submonoid.LocalizationMap.injective_iff
invertible_mk'_one_invOf 📖	mathematical	—	Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne mk' invertible_mk'_one DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	—
isDomain_localization 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	IsDomain Localization CommSemiring.toCommMonoid OreLocalization.instSemiring OreLocalization.oreSetComm	—	isDomain_of_le_nonZeroDivisors Localization.isLocalization
isDomain_of_le_nonZeroDivisors 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	IsDomain	—	Submonoid.LocalizationMap.isCancelMulZero IsDomain.toIsCancelMulZero Submonoid.LocalizationMap.nontrivial zero_notMem_nonZeroDivisors IsDomain.toNontrivial
isLocalization_iff_of_base_ringEquiv 📖	mathematical	—	IsLocalization Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.toAlgebra RingHom.comp algebraMap RingEquiv.toRingHom RingEquiv.symm	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass isLocalization_of_base_ringEquiv MulEquivClass.toMonoidWithZeroHomClass MulEquiv.instMulEquivClass RingEquivClass.toMulEquivClass MulEquivClass.instMonoidHomClass Submonoid.map_coe_toMulEquiv RingEquiv.coe_toMulEquiv_symm Submonoid.comap_equiv_eq_map_symm Submonoid.comap_map_eq_of_injective Equiv.injective RingHom.algebraMap_toAlgebra RingHom.comp_assoc RingEquiv.symm_toRingHom_comp_toRingHom RingHom.comp_id Algebra.algebra_ext
isLocalization_of_base_ringEquiv 📖	mathematical	—	IsLocalization Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHom.toAlgebra RingHom.comp algebraMap RingEquiv.toRingHom RingEquiv.symm	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm_apply_apply map_units surj Subtype.prop RingHom.algebraMap_toAlgebra RingHom.comp_apply eq_iff_exists Equiv.apply_eq_iff_eq map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.apply_symm_apply
isRegular_mk' 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	mk'	—	IsRegular.left Function.Surjective.forall mk'_surjective mul_assoc One.instNonempty mul_left_comm one_mul Submonoid.one_mem
isUnit_comp 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.comp algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.isUnit_comp
lift_comp 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	RingHom.comp lift algebraMap	—	RingHom.ext DFunLike.ext_iff Submonoid.LocalizationMap.lift_comp
lift_eq 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift algebraMap	—	Submonoid.LocalizationMap.lift_eq
lift_eq_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Submonoid.LocalizationMap.lift_eq_iff
lift_id 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike lift algebraMap map_units	—	Submonoid.LocalizationMap.lift_id
lift_injective_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift algebraMap	—	Submonoid.LocalizationMap.lift_injective_iff
lift_mk' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Units.val Units Units.instInv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Submonoid.toMonoid Units.instMulOneClass MonoidHom.instFunLike IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass RingHom.toMonoidHom	—	Submonoid.LocalizationMap.lift_mk'
lift_mk'_spec 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Submonoid.LocalizationMap.lift_mk'_spec
lift_of_comp 📖	mathematical	—	lift RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring algebraMap isUnit_comp	—	RingHom.ext isUnit_comp DFunLike.ext_iff Submonoid.LocalizationMap.lift_of_comp
lift_spec_mul_add 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CommSemiring.toCommMonoid MonoidHom.instFunLike Submonoid.LocalizationMap.lift toLocalizationMap RingHom.toMonoidHom Submonoid.LocalizationMap.sec	—	mul_comm Submonoid.instSubmonoidClass Submonoid.LocalizationMap.lift_apply mul_assoc mul_add_inv_left
lift_surjective_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	lift Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Submonoid.LocalizationMap.lift_surjective_iff
lift_unique 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike algebraMap	lift	—	RingHom.ext DFunLike.ext_iff Submonoid.LocalizationMap.lift_unique
map_comp 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	RingHom.comp map algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lift_comp map_units
map_comp_map 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	RingHom.comp map DFunLike.coe	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.ext Submonoid.LocalizationMap.map_map
map_eq 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe map algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lift_eq map_units
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.map_eq_zero_iff
map_id 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.id le_refl	DFunLike.coe map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lift_id
map_id_mk' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike map RingHom.id le_refl Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass PartialOrder.toPreorder Submonoid.instPartialOrder mk'	—	map_mk' le_refl
map_injective_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	map Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.LocalizationMap.map_injective_of_injective
map_left_cancel 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	—	Submonoid.LocalizationMap.map_left_cancel
map_map 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe map RingHom.comp	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_comp_map
map_mk' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe map mk' SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.LocalizationMap.map_mk'
map_nonZeroDivisors_le 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.map MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap nonZeroDivisors	—	Submonoid.LocalizationMap.map_nonZeroDivisors_le
map_right_cancel 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	—	Submonoid.LocalizationMap.map_right_cancel
map_smul 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe map Algebra.toSMul	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_eq
map_surjective_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	map Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.LocalizationMap.map_surjective_of_surjective
map_unique 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.comap RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass DFunLike.coe algebraMap	map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass lift_unique map_units
map_units 📖	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	—	Submonoid.IsLocalizationMap.map_units IsLocalization'.toIsLocalizationMap
mk'_add 📖	mathematical	—	mk' Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	mk'_eq_iff_eq_mul mul_comm mul_add Distrib.leftDistribClass mul_mk'_eq_mk'_of_mul mk'_add_eq_iff_add_mul_eq_mul mul_assoc add_comm map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
mk'_add_eq_iff_add_mul_eq_mul 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring mk' DFunLike.coe RingHom RingHom.instFunLike algebraMap Distrib.toMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	mk'_spec map_units right_distrib Distrib.rightDistribClass
mk'_cancel 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	Submonoid.LocalizationMap.mk'_cancel
mk'_eq_iff_eq 📖	mathematical	—	mk' DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.mk'_eq_iff_eq
mk'_eq_iff_eq' 📖	mathematical	—	mk' DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.mk'_eq_iff_eq'
mk'_eq_iff_eq_mul 📖	mathematical	—	mk' DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.mk'_eq_iff_eq_mul
mk'_eq_iff_mk'_eq 📖	mathematical	—	mk'	—	Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq
mk'_eq_mul_mk'_one 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submonoid.LocalizationMap.mul_mk'_one_eq_mk'
mk'_eq_of_eq 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	mk'	—	Submonoid.LocalizationMap.mk'_eq_of_eq
mk'_eq_of_eq' 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	mk'	—	Submonoid.LocalizationMap.mk'_eq_of_eq'
mk'_eq_zero_iff 📖	mathematical	—	mk' MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.mk'_eq_zero_iff
mk'_mul 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	Submonoid.LocalizationMap.mk'_mul
mk'_mul_cancel_left 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Submonoid.LocalizationMap.mk'_mul_cancel_left
mk'_mul_cancel_right 📖	mathematical	—	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Submonoid.LocalizationMap.mk'_mul_cancel_right
mk'_mul_mk'_eq_one 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mk'_mul mul_comm mk'_self
mk'_mul_mk'_eq_one' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring mk' AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mk'_mul_mk'_eq_one
mk'_neg 📖	mathematical	—	mk' CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	eq_mk'_iff_mul_eq neg_mul map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass mk'_spec
mk'_one 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.one DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Submonoid.LocalizationMap.mk'_one
mk'_pow 📖	mathematical	—	mk' Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike SubmonoidClass.nPow Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mk'_spec
mk'_sec 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike sec	—	Submonoid.LocalizationMap.mk'_sec
mk'_self 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	mk' AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submonoid.LocalizationMap.mk'_self
mk'_self' 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submonoid.LocalizationMap.mk'_self'
mk'_self'' 📖	mathematical	—	mk' Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mk'_self'
mk'_spec 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring mk' DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.mk'_spec
mk'_spec' 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike mk'	—	Submonoid.LocalizationMap.mk'_spec'
mk'_spec'_mk 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap mk'	—	mk'_spec'
mk'_spec_mk 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring mk' DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	mk'_spec
mk'_sub 📖	mathematical	—	mk' CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	sub_eq_add_neg mk'_neg mk'_add neg_mul
mk'_surjective 📖	mathematical	—	mk'	—	surj eq_mk'_iff_mul_eq
mk'_zero 📖	mathematical	—	mk' MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Submonoid.LocalizationMap.mk'_zero
monoidHom_ext 📖	—	MonoidHom.comp MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toMulOneClass MonoidHomClass.toMonoidHom RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap	—	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.LocalizationMap.epic_of_localizationMap
mul_add_inv_left 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul Units.val Units Units.instInv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Submonoid.toMonoid Units.instMulOneClass MonoidHom.instFunLike IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass RingHom.toMonoidHom	—	Submonoid.instSubmonoidClass mul_comm one_mul Units.inv_mul mul_assoc mul_add Distrib.leftDistribClass Units.inv_mul_eq_iff_eq_mul Units.inv_mul_cancel_left IsUnit.coe_liftRight
mul_mk'_eq_mk'_of_mul 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap mk'	—	Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul
ne_zero_of_mk'_ne_zero 📖	—	—	—	—	mk'_zero
noZeroDivisors 📖	mathematical	—	NoZeroDivisors Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Submonoid.LocalizationMap.noZeroDivisors
nonZeroDivisors_le_comap 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap	—	Submonoid.LocalizationMap.nonZeroDivisors_le_comap
of_le 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom RingHom.instFunLike algebraMap	IsLocalization	—	surj eq_iff_exists
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 isUnit_of_dvd_unit map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_units
ringEquivOfRingEquiv_apply 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass RingEquiv.toMonoidHom	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivOfRingEquiv RingHom RingHom.instFunLike map RingHomClass.toRingHom	—	MonoidHom.instMonoidHomClass
ringEquivOfRingEquiv_eq 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass RingEquiv.toMonoidHom	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivOfRingEquiv RingHom RingHom.instFunLike algebraMap	—	MonoidHom.instMonoidHomClass map_eq
ringEquivOfRingEquiv_eq_map 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass RingEquiv.toMonoidHom	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass ringEquivOfRingEquiv map Submonoid.le_comap_of_map_le RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_of_eq Submonoid PartialOrder.toPreorder Submonoid.instPartialOrder	—	MonoidHom.instMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
ringEquivOfRingEquiv_mk' 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass RingEquiv.toMonoidHom	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivOfRingEquiv mk' Submonoid SetLike.instMembership Submonoid.instSetLike	—	MonoidHom.instMonoidHomClass Set.mem_image_of_mem map_mk'
ringEquivOfRingEquiv_symm 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	RingEquiv.symm ringEquivOfRingEquiv	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
ringEquivOfRingEquiv_symm_apply 📖	mathematical	Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass RingEquiv.toMonoidHom	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringEquivOfRingEquiv RingHom RingHom.instFunLike map RingHomClass.toRingHom	—	MonoidHom.instMonoidHomClass
ringHom_ext 📖	—	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring algebraMap	—	—	RingHom.coe_monoidHom_injective monoidHom_ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MonoidHom.ext RingHom.congr_fun
sec_fst_ne_zero 📖	—	—	—	—	mk'_sec mk'_zero
sec_snd_ne_zero 📖	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	—	—	nonZeroDivisors.coe_ne_zero
sec_spec 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike sec	—	surj
sec_spec' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike sec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	mul_comm sec_spec
smul_bijective 📖	mathematical	—	Function.Bijective Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul Algebra.toSMul	—	Algebra.smul_def IsUnit.smul_bijective map_units
smul_mk' 📖	mathematical	—	Algebra.toSMul CommSemiring.toSemiring mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	one_mul mk'_mul mk'_one Algebra.smul_def
smul_mk'_one 📖	mathematical	—	Algebra.toSMul CommSemiring.toSemiring mk' AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	smul_mk' mul_one
smul_mk'_self 📖	mathematical	—	Algebra.toSMul CommSemiring.toSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike mk' DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	smul_mk' mk'_mul_cancel_left
subsingleton 📖	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—	Submonoid.LocalizationMap.subsingleton
subsingleton_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Submonoid.instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Submonoid.LocalizationMap.subsingleton_iff
surj 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.surj IsLocalization'.toIsLocalizationMap
surj₂ 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.LocalizationMap.surj₂
toLocalizationMap_apply 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommSemiring.toCommMonoid Submonoid.LocalizationMap.instFunLike toLocalizationMap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
toLocalizationMap_sec 📖	mathematical	—	Submonoid.LocalizationMap.sec CommSemiring.toCommMonoid toLocalizationMap sec	—	—
toLocalizationMap_toMonoidHom 📖	mathematical	—	Submonoid.LocalizationMap.toMonoidHom CommSemiring.toCommMonoid toLocalizationMap MonoidHomClass.toMonoidHom MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHomClass.toMonoidWithZeroHom RingHom RingHom.instFunLike RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap	—	—
to_map_eq_zero_iff 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero	DFunLike.coe RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_eq_zero_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
to_map_ne_zero_of_mem_nonZeroDivisors 📖	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Semiring.toMonoidWithZero MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	—	to_map_eq_zero_iff nonZeroDivisors.ne_zero

IsLocalization'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsLocalizationMap 📖	mathematical	—	Submonoid.IsLocalizationMap CommSemiring.toCommMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—

Localization

Definitions

Name	Category	Theorems
instUniqueLocalization 📖	CompOp	—
mkAddMonoidHom 📖	CompOp	1 math math: mkAddMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mk 📖	mathematical	—	Localization CommSemiring.toCommMonoid OreLocalization.instAdd CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Module.toDistribMulAction Semiring.toModule Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	add_comm SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_comm OreLocalization.oreDiv_add_oreDiv
add_mk_self 📖	mathematical	—	Localization CommSemiring.toCommMonoid OreLocalization.instAdd CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Module.toDistribMulAction Semiring.toModule Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	mk_eq_mk_iff r_eq_r' Con.symm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf 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_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors Localization CommSemiring.toCommMonoid OreLocalization.instMul CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toMulAction	—	IsLocalization.noZeroDivisors isLocalization
isLocalization 📖	mathematical	—	IsLocalization Localization CommSemiring.toCommMonoid OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring Algebra.id	—	Submonoid.LocalizationMap.isLocalizationMap
mkAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Localization CommSemiring.toCommMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instAddMonoid CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Module.toDistribMulAction Semiring.toModule AddMonoidHom.instFunLike mkAddMonoidHom	—	—
mk_algebraMap 📖	mathematical	—	CommSemiring.toCommMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one Localization OreLocalization.instSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra	—	isLocalization mk_eq_mk' IsLocalization.mk'_eq_iff_eq_mul Submonoid.coe_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
mk_eq_mk' 📖	mathematical	—	CommSemiring.toCommMonoid IsLocalization.mk' Localization OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring Algebra.id isLocalization	—	mk_eq_monoidOf_mk'
mk_eq_mk'_apply 📖	mathematical	—	CommSemiring.toCommMonoid IsLocalization.mk' Localization OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring Algebra.id isLocalization	—	isLocalization mk_eq_monoidOf_mk'_apply IsLocalization.mk'.eq_1 toLocalizationMap_eq_monoidOf
mk_list_sum 📖	mathematical	—	CommSemiring.toCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Localization OreLocalization.instAdd CommMonoid.toMonoid OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule OreLocalization.instZero Monoid.toMulAction	—	map_list_sum AddMonoidHom.instAddMonoidHomClass
mk_multiset_sum 📖	mathematical	—	CommSemiring.toCommMonoid Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Localization OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm Module.toDistribMulAction Semiring.toModule Multiset.map	—	AddMonoidHom.map_multiset_sum
mk_one_eq_algebraMap 📖	mathematical	—	CommSemiring.toCommMonoid Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one DFunLike.coe RingHom Localization Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—
mk_sum 📖	mathematical	—	CommSemiring.toCommMonoid Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Localization OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid OreLocalization.oreSetComm Module.toDistribMulAction Semiring.toModule	—	map_sum AddMonoidHom.instAddMonoidHomClass
monoidOf_eq_algebraMap 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap CommSemiring.toCommMonoid Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm Submonoid.LocalizationMap.instFunLike monoidOf RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring OreLocalization.instSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—
neg_mk 📖	mathematical	—	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 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	OreLocalization.neg_def
sub_mk 📖	mathematical	—	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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	sub_eq_add_neg add_comm mul_neg
toLocalizationMap_eq_monoidOf 📖	mathematical	—	IsLocalization.toLocalizationMap Localization CommSemiring.toCommMonoid OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring Algebra.id isLocalization monoidOf	—	isLocalization

(root)

Definitions

Name	Category	Theorems
IsLocalization' 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalization_iff 📖	mathematical	—	IsLocalization IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	isLocalization_iff_isLocalizationMap Submonoid.isLocalizationMap_iff
isLocalization_iff_isLocalizationMap 📖	mathematical	—	IsLocalization Submonoid.IsLocalizationMap CommSemiring.toCommMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—

---

← Back to Index