Basic

📁 Source: Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Statistics

Metric	Count
Definitions AddLocalization, addMonoidOf, decidableEq, liftOn, liftOn₂, mk, mkHom, r, r', rec, recOnSubsingleton₂, toLocalizationMap, IsLocalizationMap, LocalizationMap, instFunLike, mk', sec, toAddHom, toAddMonoidHom, decidableEq, liftOn, liftOn₂, mk, mkHom, monoidOf, r, r', rec, recOnSubsingleton₂, toLocalizationMap, equivMonoidLocalization, localizationMap, IsLocalizationMap, LocalizationMap, instFunLike, mk', sec, toMonoidHom, toMulHom	39
Theorems ind, induction_on, induction_on₂, induction_on₃, instIsAddTorsionFree, liftOn_mk, liftOn_mk', liftOn₂_mk, liftOn₂_mk', mkHom_apply, mkHom_surjective, mk_add, mk_eq_addMonoidOf_mk', mk_eq_addMonoidOf_mk'_apply, mk_eq_mk_iff, mk_eq_mk_iff', mk_left_injective, mk_nsmul, mk_self, mk_self_mk, mk_sum, mk_zero, mk_zero_eq_addMonoidOf_mk, ndrec_mk, r_eq_r', r_iff_exists, r_iff_oreEqv_r, r_of_eq, zero_rel, addEquiv_comp, exists_of_eq, map_addUnits, map_zero, surj, add_mk'_eq_mk'_of_add, add_mk'_zero_eq_mk', add_neg, add_neg_left, add_neg_right, epic_of_localizationMap, eq, eq', eq_iff_eq, eq_iff_exists, eq_mk'_iff_add_eq, exists_of_eq, exists_of_sec_mk', ext, ext_iff, injective_iff, instAddMonoidHomClass, instIsCancelAddLocalization, instNontrivialLocalizationOfIsCancelAdd, isAddUnit_comp, isCancelAdd, isLocalizationMap, map_addUnits, map_isAddRegular, map_left_cancel, map_right_cancel, mk'_add, mk'_add_cancel_left, mk'_add_cancel_right, mk'_add_eq_mk'_of_add, mk'_cancel, mk'_eq_iff_eq, mk'_eq_iff_eq', mk'_eq_iff_eq_add, mk'_eq_iff_mk'_eq, mk'_eq_of_eq, mk'_eq_of_eq', mk'_eq_of_same, mk'_sec, mk'_self, mk'_self', mk'_spec, mk'_spec', mk'_surjective, mk'_zero, neg_inj, neg_unique, sec_spec, sec_spec', subsingleton_of_subsingleton, surj, surj₂, toAddMonoidHom_apply, toAddMonoidHom_injective, top_injective_iff, isLocalizationMap_id, isLocalizationMap_iff, isLocalizationMap_iff_bijective, isLocalizationMap_nat_int, isLocalizationMap_of_addGroup, isLocalizationMap_top_nat_int, ind, induction_on, induction_on₂, induction_on₃, instIsMulTorsionFree, instSMulCommClassOfIsScalarTower, liftOn_mk, liftOn_mk', liftOn₂_mk, liftOn₂_mk', mkHom_apply, mkHom_surjective, mk_eq_mk_iff, mk_eq_mk_iff', mk_eq_monoidOf_mk', mk_eq_monoidOf_mk'_apply, mk_left_injective, mk_mul, mk_one, mk_one_eq_monoidOf_mk, mk_pow, mk_prod, mk_self, mk_self_mk, ndrec_mk, one_rel, r_eq_r', r_iff_exists, r_iff_oreEqv_r, r_of_eq, smul_mk, exists_of_eq, map_one, map_units, mulEquiv_comp, surj, epic_of_localizationMap, eq, eq', eq_iff_eq, eq_iff_exists, eq_mk'_iff_mul_eq, exists_of_eq, exists_of_sec_mk', ext, ext_iff, injective_iff, instIsCancelMulLocalization, instMonoidHomClass, instNontrivialLocalizationOfIsCancelMul, instSubsingletonLocalization, inv_inj, inv_unique, isCancelMul, isLocalizationMap, isUnit_comp, map_isRegular, map_left_cancel, map_right_cancel, map_units, mk'_cancel, mk'_eq_iff_eq, mk'_eq_iff_eq', mk'_eq_iff_eq_mul, mk'_eq_iff_mk'_eq, mk'_eq_of_eq, mk'_eq_of_eq', mk'_eq_of_same, mk'_mul, mk'_mul_cancel_left, mk'_mul_cancel_right, mk'_mul_eq_mk'_of_mul, mk'_one, mk'_sec, mk'_self, mk'_self', mk'_spec, mk'_spec', mk'_surjective, mul_inv, mul_inv_left, mul_inv_right, mul_mk'_eq_mk'_of_mul, mul_mk'_one_eq_mk', sec_spec, sec_spec', subsingleton_of_subsingleton, surj, surj₂, toMonoidHom_apply, toMonoidHom_injective, top_injective_iff, isLocalizationMap_id, isLocalizationMap_iff, isLocalizationMap_iff_bijective, isLocalizationMap_of_group	191
Total	230

AddLocalization

Definitions

Name	Category	Theorems
addMonoidOf 📖	CompOp	11 math math: liftOn_mk', mk_zero_eq_addMonoidOf_mk, addEquivOfQuotient_mk', mk_eq_addMonoidOf_mk', addEquivOfQuotient_apply, addEquivOfQuotient_symm_mk', liftOn₂_mk', Algebra.GrothendieckAddGroup.lift_apply, addEquivOfQuotient_addMonoidOf, addEquivOfQuotient_symm_addMonoidOf, mk_eq_addMonoidOf_mk'_apply
decidableEq 📖	CompOp	—
liftOn 📖	CompOp	2 math math: liftOn_mk', liftOn_mk
liftOn₂ 📖	CompOp	2 math math: liftOn₂_mk, liftOn₂_mk'
mk 📖	CompOp	—
mkHom 📖	CompOp	2 math math: mkHom_apply, mkHom_surjective
r 📖	CompOp	7 math math: r_of_eq, r_iff_exists, zero_rel, AddSubmonoid.LocalizationMap.eq', mk_eq_mk_iff, r_eq_r', r_iff_oreEqv_r
r' 📖	CompOp	1 math math: r_eq_r'
rec 📖	CompOp	—
recOnSubsingleton₂ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind 📖	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	mk_eq_mk_iff
induction_on 📖	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	ind
induction_on₂ 📖	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	induction_on
induction_on₃ 📖	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	induction_on₂ induction_on
instIsAddTorsionFree 📖	mathematical	—	IsAddTorsionFree AddLocalization AddOreLocalization.instAddMonoid AddCommMonoid.toAddMonoid AddOreLocalization.addOreSetComm	—	mk_eq_mk_iff r_iff_exists AddSubmonoid.instAddSubmonoidClass mk_nsmul nsmul_right_injective zero_nsmul nsmul_add succ_nsmul add_assoc
liftOn_mk 📖	mathematical	—	liftOn	—	—
liftOn_mk' 📖	mathematical	—	liftOn AddSubmonoid.LocalizationMap.mk' AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm addMonoidOf	—	mk_eq_addMonoidOf_mk'
liftOn₂_mk 📖	mathematical	—	liftOn₂	—	—
liftOn₂_mk' 📖	mathematical	—	liftOn₂ AddSubmonoid.LocalizationMap.mk' AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm addMonoidOf	—	mk_eq_addMonoidOf_mk'
mkHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddLocalization AddZeroClass.toAddZero Prod.instAddZeroClass AddSubmonoid.toAddZeroClass AddOreLocalization.instAddMonoid AddOreLocalization.addOreSetComm AddMonoidHom.instFunLike mkHom	—	—
mkHom_surjective 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddLocalization DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Prod.instAddZeroClass AddSubmonoid.toAddZeroClass AddOreLocalization.instAddMonoid AddOreLocalization.addOreSetComm AddMonoidHom.instFunLike mkHom	—	—
mk_add 📖	mathematical	—	AddLocalization AddOreLocalization.instAdd AddCommMonoid.toAddMonoid AddOreLocalization.addOreSetComm AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.add	—	AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass AddOreLocalization.oreSub_add_oreSub add_comm
mk_eq_addMonoidOf_mk' 📖	mathematical	—	AddSubmonoid.LocalizationMap.mk' AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm addMonoidOf	—	mk_eq_addMonoidOf_mk'_apply
mk_eq_addMonoidOf_mk'_apply 📖	mathematical	—	AddSubmonoid.LocalizationMap.mk' AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm addMonoidOf	—	AddSubmonoid.LocalizationMap.map_addUnits AddSubmonoid.instAddSubmonoidClass AddSubmonoid.LocalizationMap.add_neg_right mk_add AddSubmonoidClass.toAddMemClass add_comm add_zero mk_eq_mk_iff AddCon.symm AddCon.add AddCon.refl zero_rel
mk_eq_mk_iff 📖	mathematical	—	DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp r	—	AddOreLocalization.oreSub_eq_iff r_iff_oreEqv_r
mk_eq_mk_iff' 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	mk_eq_mk_iff r_iff_exists add_left_cancel_iff IsCancelAdd.toIsLeftCancelAdd Zero.instNonempty
mk_left_injective 📖	mathematical	—	AddLocalization	—	mk_eq_mk_iff r_iff_exists IsCancelAdd.toIsLeftCancelAdd Zero.instNonempty
mk_nsmul 📖	mathematical	—	AddLocalization AddMonoid.toNatSMul AddOreLocalization.instAddMonoid AddCommMonoid.toAddMonoid AddOreLocalization.addOreSetComm AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoidClass.nSMul AddSubmonoid.instAddSubmonoidClass	—	AddSubmonoid.instAddSubmonoidClass zero_nsmul mk_zero succ_nsmul mk_add
mk_self 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddLocalization AddOreLocalization.instZero AddOreLocalization.addOreSetComm AddMonoid.toAddAction AddZero.toZero AddZeroClass.toAddZero	—	mk_zero mk_eq_mk_iff zero_rel
mk_self_mk 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	AddLocalization AddOreLocalization.instZero AddOreLocalization.addOreSetComm AddMonoid.toAddAction AddZero.toZero AddZeroClass.toAddZero	—	mk_self
mk_sum 📖	mathematical	—	Finset.sum AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.toAddCommMonoid	—	Finset.induction_on mk_zero Finset.sum_insert mk_add
mk_zero 📖	mathematical	—	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.zero AddLocalization AddOreLocalization.instZero AddOreLocalization.addOreSetComm AddMonoid.toAddAction	—	AddOreLocalization.zero_def
mk_zero_eq_addMonoidOf_mk 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.zero DFunLike.coe AddSubmonoid.LocalizationMap AddLocalization AddOreLocalization.instAddCommMonoid AddOreLocalization.addOreSetComm AddSubmonoid.LocalizationMap.instFunLike addMonoidOf	—	—
ndrec_mk 📖	—	AddLocalization DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp r mk_eq_mk_iff	—	—	mk_eq_mk_iff
r_eq_r' 📖	mathematical	—	r r'	—	le_antisymm sInf_le add_zero zero_add le_sInf AddCon.trans AddCon.add AddCon.refl AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass add_assoc add_comm AddCon.symm
r_iff_exists 📖	mathematical	—	DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp r	—	r_eq_r'
r_iff_oreEqv_r 📖	mathematical	—	DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp r AddOreLocalization.oreEqv AddOreLocalization.addOreSetComm AddMonoid.toAddAction	—	r_iff_exists AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass add_assoc add_right_comm add_comm
r_of_eq 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	DFunLike.coe AddCon Prod.instAdd AddSubmonoid.add AddCon.instFunLikeForallProp r	—	r_iff_exists
zero_rel 📖	mathematical	—	DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp r Prod.instZero AddZero.toZero AddSubmonoid.zero	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
toLocalizationMap 📖	CompOp	—

AddSubmonoid

Definitions

Name	Category	Theorems
IsLocalizationMap 📖	CompData	7 math math: isLocalizationMap_iff, isLocalizationMap_of_addGroup, isLocalizationMap_iff_bijective, isLocalizationMap_nat_int, isLocalizationMap_top_nat_int, isLocalizationMap_id, LocalizationMap.isLocalizationMap
LocalizationMap 📖	CompData	46 math math: LocalizationMap.mk'_spec, LocalizationMap.mk'_eq_iff_eq_add, LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply, LocalizationMap.addEquivOfAddEquiv_eq, LocalizationMap.surj₂, LocalizationMap.map_add_right, LocalizationMap.eq_iff_exists, LocalizationMap.injective_iff, LocalizationMap.mk'_spec', LocalizationMap.ofAddEquivOfLocalizations_eq_iff_eq, LocalizationMap.mk'_eq_iff_eq', LocalizationMap.mk'_zero, LocalizationMap.map_spec, LocalizationMap.of_addEquivOfAddEquiv_apply, LocalizationMap.map_add_left, LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply', LocalizationMap.lift_injective_iff, AddLocalization.mk_zero_eq_addMonoidOf_mk, LocalizationMap.sec_spec', LocalizationMap.map_eq, LocalizationMap.ofAddEquivOfDom_apply, LocalizationMap.add_mk'_zero_eq_mk', LocalizationMap.ofAddEquivOfLocalizations_apply, LocalizationMap.surj, LocalizationMap.lift_eq, LocalizationMap.add_mk'_eq_mk'_of_add, mem_subPairs, LocalizationMap.addEquivOfLocalizations_right_inv_apply, LocalizationMap.toAddMonoidHom_injective, LocalizationMap.mk'_add_eq_mk'_of_add, LocalizationMap.eq_mk'_iff_add_eq, LocalizationMap.toAddMonoidHom_apply, LocalizationMap.ext_iff, LocalizationMap.mk'_add_cancel_left, LocalizationMap.ofAddEquivOfDom_comp_symm, AddLocalization.addEquivOfQuotient_addMonoidOf, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, LocalizationMap.ofAddEquivOfDom_comp, LocalizationMap.instAddMonoidHomClass, LocalizationMap.eq_iff_eq, LocalizationMap.sec_spec, LocalizationMap.map_isAddRegular, LocalizationMap.mk'_eq_iff_eq, LocalizationMap.mk'_add_cancel_right, LocalizationMap.map_addUnits, LocalizationMap.top_injective_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalizationMap_id 📖	mathematical	—	IsLocalizationMap AddCommGroup.toAddCommMonoid	—	isLocalizationMap_iff_bijective AddHom.addHomClass Function.bijective_id
isLocalizationMap_iff 📖	mathematical	—	IsLocalizationMap IsAddUnit AddCommMonoid.toAddMonoid AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership instSetLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
isLocalizationMap_iff_bijective 📖	mathematical	—	IsLocalizationMap AddCommGroup.toAddCommMonoid DFunLike.coe Function.Bijective	—	IsLocalizationMap.exists_of_eq add_left_cancel AddLeftCancelSemigroup.toIsLeftCancelAdd IsLocalizationMap.surj sub_eq_add_neg map_add add_assoc add_neg_cancel IsLocalizationMap.map_zero add_zero IsAddUnit.map AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddGroup.isAddUnit AddEquiv.map_zero Zero.instNonempty
isLocalizationMap_nat_int 📖	mathematical	—	IsLocalizationMap Nat.instAddCommMonoid Int.instAddCommMonoid	—	isLocalizationMap_of_addGroup ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass instAddSubmonoidClass bot_or_exists_ne_zero nsmul_mem
isLocalizationMap_of_addGroup 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	IsLocalizationMap AddCommGroup.toAddCommMonoid	—	AddGroup.isAddUnit sub_add_cancel Zero.instNonempty
isLocalizationMap_top_nat_int 📖	mathematical	—	IsLocalizationMap Nat.instAddCommMonoid Int.instAddCommMonoid Top.top AddSubmonoid AddMonoid.toAddZeroClass Nat.instAddMonoid instTop	—	isLocalizationMap_nat_int top_ne_bot instNontrivial Nat.instNontrivial

AddSubmonoid.IsLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquiv_comp 📖	mathematical	AddSubmonoid.IsLocalizationMap	DFunLike.coe EquivLike.toFunLike	—	IsAddUnit.map AddEquivClass.instAddMonoidHomClass map_addUnits surj AddEquiv.injective map_add AddMonoidHomClass.toAddHomClass AddEquiv.instAddEquivClass AddEquivClass.coe_symm_apply_apply exists_of_eq EquivLike.injective
exists_of_eq 📖	mathematical	AddSubmonoid.IsLocalizationMap	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—
map_addUnits 📖	mathematical	AddSubmonoid.IsLocalizationMap	IsAddUnit AddCommMonoid.toAddMonoid AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike	—	—
map_zero 📖	mathematical	AddSubmonoid.IsLocalizationMap DFunLike.coe	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_addUnits add_zero map_add
surj 📖	mathematical	AddSubmonoid.IsLocalizationMap	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—

AddSubmonoid.LocalizationMap

Definitions

Name	Category	Theorems
instFunLike 📖	CompOp	47 math math: mk'_spec, mk'_eq_iff_eq_add, symm_comp_ofAddEquivOfLocalizations_apply, addEquivOfAddEquiv_eq, surj₂, map_add_right, eq_iff_exists, injective_iff, mk'_spec', ofAddEquivOfLocalizations_eq_iff_eq, mk'_eq_iff_eq', mk'_zero, map_spec, of_addEquivOfAddEquiv_apply, map_add_left, symm_comp_ofAddEquivOfLocalizations_apply', lift_injective_iff, AwayMap.lift_comp, AddLocalization.mk_zero_eq_addMonoidOf_mk, sec_spec', map_eq, ofAddEquivOfDom_apply, add_mk'_zero_eq_mk', ofAddEquivOfLocalizations_apply, surj, lift_eq, add_mk'_eq_mk'_of_add, AddSubmonoid.mem_subPairs, addEquivOfLocalizations_right_inv_apply, mk'_add_eq_mk'_of_add, eq_mk'_iff_add_eq, toAddMonoidHom_apply, ext_iff, mk'_add_cancel_left, ofAddEquivOfDom_comp_symm, AddLocalization.addEquivOfQuotient_addMonoidOf, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, ofAddEquivOfDom_comp, instAddMonoidHomClass, eq_iff_eq, sec_spec, map_isAddRegular, mk'_eq_iff_eq, mk'_add_cancel_right, map_addUnits, top_injective_iff, AwayMap.lift_eq
mk' 📖	CompOp	40 math math: mk'_spec, mk'_eq_iff_eq_add, mk'_eq_of_eq', AddLocalization.liftOn_mk', addEquivOfAddEquiv_mk', mk'_spec', mk'_eq_iff_eq', mk'_zero, mk'_add, lift_eq_iff, mk'_surjective, mk'_self', lift_mk'_spec, mk'_eq_of_eq, AddLocalization.addEquivOfQuotient_mk', AddLocalization.mk_eq_addMonoidOf_mk', mk'_eq_iff_mk'_eq, add_mk'_zero_eq_mk', add_mk'_eq_mk'_of_add, AddLocalization.addEquivOfQuotient_mk, eq', AddLocalization.addEquivOfQuotient_symm_mk', mk'_add_eq_mk'_of_add, eq_mk'_iff_add_eq, mk'_add_cancel_left, AddLocalization.liftOn₂_mk', exists_of_sec_mk', AddLocalization.addEquivOfQuotient_symm_mk, AddLocalization.Away.mk_eq_addMonoidOf_mk', mk'_self, eq, lift_localizationMap_mk', mk'_cancel, AddLocalization.mk_eq_addMonoidOf_mk'_apply, mk'_eq_of_same, mk'_eq_iff_eq, mk'_add_cancel_right, lift_mk', mk'_sec, map_mk'
sec 📖	CompOp	13 math math: map_add_right, map_spec, map_add_left, lift_apply, sec_spec', lift_spec_add, lift_spec, exists_of_sec_mk', Algebra.GrothendieckAddGroup.lift_apply, lift_add_right, sec_spec, mk'_sec, lift_add_left
toAddHom 📖	CompOp	1 math math: isLocalizationMap
toAddMonoidHom 📖	CompOp	18 math math: ofAddEquivOfLocalizations_eq, addEquivOfLocalizations_symm_apply, isAddUnit_comp, lift_of_comp, AddLocalization.addEquivOfQuotient_apply, map_comp, toAddMonoidHom_injective, lift_comp, lift_comp_lift, lift_comp_lift_eq, toAddMonoidHom_apply, ofAddEquivOfLocalizations_comp, ofAddEquivOfDom_eq, lift_id, lift_localizationMap_mk', of_addEquivOfAddEquiv, lift_left_inverse, addEquivOfLocalizations_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mk'_eq_mk'_of_add 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike mk'	—	mk'_zero mk'_add zero_add
add_mk'_zero_eq_mk' 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike mk' AddZero.toZero	—	add_mk'_eq_mk'_of_add add_zero
add_neg 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	AddZero.toAdd AddUnits.val AddUnits AddUnits.instNeg AddSubmonoid.toAddMonoid AddUnits.instAddZeroClass IsAddUnit.liftRight AddMonoidHom.restrict AddSubmonoid.instAddSubmonoidClass	—	AddSubmonoid.instAddSubmonoidClass add_neg_right add_assoc add_comm add_neg_left AddMonoidHom.map_add
add_neg_left 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	AddZero.toAdd AddUnits.val AddUnits AddUnits.instNeg AddSubmonoid.toAddMonoid AddUnits.instAddZeroClass IsAddUnit.liftRight AddMonoidHom.restrict AddSubmonoid.instAddSubmonoidClass	—	AddSubmonoid.instAddSubmonoidClass add_comm AddUnits.neg_add_eq_iff_eq_add
add_neg_right 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	AddZero.toAdd AddUnits.val AddUnits AddUnits.instNeg AddSubmonoid.toAddMonoid AddUnits.instAddZeroClass IsAddUnit.liftRight AddMonoidHom.restrict AddSubmonoid.instAddSubmonoidClass	—	AddSubmonoid.instAddSubmonoidClass add_neg_left add_comm
epic_of_localizationMap 📖	—	AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddMonoidHom	—	—	AddMonoidHom.ext surj IsAddUnit.map AddMonoidHom.instAddMonoidHomClass map_addUnits AddMonoidHom.map_add
eq 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	mk'_eq_iff_eq eq_iff_exists
eq' 📖	mathematical	—	mk' DFunLike.coe AddCon AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike Prod.instAdd AddZero.toAdd AddZeroClass.toAddZero AddSubmonoid.add AddCon.instFunLikeForallProp AddLocalization.r	—	eq AddLocalization.r_iff_exists
eq_iff_eq 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	eq_iff_exists
eq_iff_exists 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	AddSubmonoid.IsLocalizationMap.exists_of_eq isLocalizationMap map_addUnits map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass
eq_mk'_iff_add_eq 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	mk'_spec map_addUnits mk'.eq_1 AddSubmonoid.instAddSubmonoidClass add_neg_right
exists_of_eq 📖	mathematical	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	AddSubmonoid.IsLocalizationMap.exists_of_eq isLocalizationMap
exists_of_sec_mk' 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike sec mk'	—	eq_iff_exists mk'_eq_iff_eq mk'_sec
ext 📖	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	ext
injective_iff 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike IsAddRegular AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	AddCommute.isAddRegular_iff AddCommute.all eq_iff_exists forall₂_swap
instAddMonoidHomClass 📖	mathematical	—	AddMonoidHomClass AddSubmonoid.LocalizationMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike	—	AddHom.map_add AddMonoidHom.map_zero
instIsCancelAddLocalization 📖	mathematical	—	IsCancelAdd AddLocalization AddOreLocalization.instAdd AddCommMonoid.toAddMonoid AddOreLocalization.addOreSetComm	—	isCancelAdd
instNontrivialLocalizationOfIsCancelAdd 📖	mathematical	—	Nontrivial AddLocalization	—	Function.Injective.nontrivial injective_iff IsAddRegular.all
isAddUnit_comp 📖	mathematical	—	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddMonoidHom.comp toAddMonoidHom AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	AddSubmonoid.instAddSubmonoidClass map_addUnits IsAddUnit.coe_liftRight
isCancelAdd 📖	mathematical	—	IsCancelAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	isCancelAdd_iff_forall_isAddRegular AddCommute.isAddRegular_iff AddCommute.all AddCommute.isAddRightRegular_iff surj IsAddRightRegular.of_add IsAddRegular.right map_isAddRegular
isLocalizationMap 📖	mathematical	—	AddSubmonoid.IsLocalizationMap AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup toAddHom	—	—
map_addUnits 📖	mathematical	—	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike	—	AddSubmonoid.IsLocalizationMap.map_addUnits isLocalizationMap
map_isAddRegular 📖	mathematical	IsAddRegular AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	AddCommute.isAddRegular_iff AddCommute.all surj map_addUnits AddSubmonoid.coe_add map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass add_assoc add_right_comm eq_iff_exists IsAddRegular.left add_left_comm
map_left_cancel 📖	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	map_right_cancel add_comm
map_right_cancel 📖	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	—	map_addUnits map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass
mk'_add 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.add	—	AddSubmonoid.instAddSubmonoidClass map_addUnits add_neg_left map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass AddMonoidHom.instAddMonoidHomClass add_add_add_comm add_left_comm IsAddUnit.add_val_neg add_zero
mk'_add_cancel_left 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	add_comm mk'_add_cancel_right
mk'_add_cancel_right 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	add_mk'_zero_eq_mk' map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass add_assoc mk'_self' add_zero
mk'_add_eq_mk'_of_add 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid mk' DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	add_comm add_mk'_eq_mk'_of_add
mk'_cancel 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.add	—	mk'_eq_of_eq' AddSubmonoid.coe_add add_comm add_assoc
mk'_eq_iff_eq 📖	mathematical	—	mk' DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass mk'_eq_iff_eq_add add_assoc mk'_spec' add_comm map_addUnits mk'.eq_1 AddSubmonoid.instAddSubmonoidClass add_neg_right toAddMonoidHom_apply
mk'_eq_iff_eq' 📖	mathematical	—	mk' DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	mk'_eq_iff_eq add_comm
mk'_eq_iff_eq_add 📖	mathematical	—	mk' DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	eq_mk'_iff_add_eq
mk'_eq_iff_mk'_eq 📖	mathematical	—	mk'	—	eq'
mk'_eq_of_eq 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	mk'	—	mk'_eq_iff_eq
mk'_eq_of_eq' 📖	mathematical	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	mk'	—	mk'_eq_of_eq add_comm
mk'_eq_of_same 📖	mathematical	—	mk' AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	mk'_eq_iff_eq' map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass eq_iff_exists map_addUnits
mk'_sec 📖	mathematical	—	mk' AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike sec	—	map_addUnits sec_spec AddSubmonoid.instAddSubmonoidClass add_neg_left add_comm
mk'_self 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike	mk' AddZero.toZero AddZeroClass.toAddZero	—	mk'_self'
mk'_self' 📖	mathematical	—	mk' AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddZero.toZero AddZeroClass.toAddZero	—	map_addUnits AddSubmonoid.instAddSubmonoidClass add_neg_left add_zero
mk'_spec 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid mk' DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	map_addUnits add_assoc add_comm AddSubmonoid.instAddSubmonoidClass add_neg_left
mk'_spec' 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike mk'	—	add_comm mk'_spec
mk'_surjective 📖	mathematical	—	mk'	—	mk'_sec
mk'_zero 📖	mathematical	—	mk' AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.zero DFunLike.coe AddSubmonoid.LocalizationMap instFunLike	—	map_addUnits mk'.eq_1 map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass add_zero
neg_inj 📖	—	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddUnits AddUnits.instNeg AddSubmonoid.toAddMonoid AddUnits.instAddZeroClass IsAddUnit.liftRight AddMonoidHom.restrict AddSubmonoid.instAddSubmonoidClass	—	—	AddSubmonoid.instAddSubmonoidClass add_zero add_neg_left AddUnits.neg_add
neg_unique 📖	mathematical	IsAddUnit AddCommMonoid.toAddMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike AddZero.toAdd AddZero.toZero	AddUnits.val AddUnits AddUnits.instNeg AddSubmonoid.toAddMonoid AddUnits.instAddZeroClass IsAddUnit.liftRight AddMonoidHom.restrict AddSubmonoid.instAddSubmonoidClass	—	AddSubmonoid.instAddSubmonoidClass zero_add AddUnits.val_add add_neg_left
sec_spec 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike sec	—	surj
sec_spec' 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike sec AddZero.toAdd AddZeroClass.toAddZero	—	add_comm sec_spec
subsingleton_of_subsingleton 📖	—	—	—	—	mk'_surjective instSubsingletonSubtype_mathlib
surj 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	AddSubmonoid.IsLocalizationMap.surj isLocalizationMap
surj₂ 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe AddSubmonoid.LocalizationMap instFunLike AddSubmonoid SetLike.instMembership AddSubmonoid.instSetLike	—	surj map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass add_assoc add_left_comm
toAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike toAddMonoidHom AddSubmonoid.LocalizationMap instFunLike	—	—
toAddMonoidHom_injective 📖	mathematical	—	AddSubmonoid.LocalizationMap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddMonoidHom	—	AddHom.ext isLocalizationMap
top_injective_iff 📖	mathematical	—	DFunLike.coe AddSubmonoid.LocalizationMap Top.top AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instTop instFunLike IsCancelAdd AddZero.toAdd AddZeroClass.toAddZero	—	injective_iff AddSubmonoid.mem_top isCancelAdd_iff_forall_isAddRegular

Localization

Definitions

Name	Category	Theorems
decidableEq 📖	CompOp	—
liftOn 📖	CompOp	4 math math: liftOn_zero, liftOn_mk, RatFunc.liftOn_def, liftOn_mk'
liftOn₂ 📖	CompOp	2 math math: liftOn₂_mk', liftOn₂_mk
mk 📖	CompOp	—
mkHom 📖	CompOp	2 math math: mkHom_surjective, mkHom_apply
monoidOf 📖	CompOp	13 math math: mk_eq_monoidOf_mk', mulEquivOfQuotient_symm_monoidOf, toLocalizationMap_eq_monoidOf, liftOn₂_mk', mk_one_eq_monoidOf_mk, mk_eq_monoidOf_mk'_apply, mulEquivOfQuotient_mk', monoidOf_eq_algebraMap, mulEquivOfQuotient_monoidOf, mulEquivOfQuotient_apply, Algebra.GrothendieckGroup.lift_apply, liftOn_mk', mulEquivOfQuotient_symm_mk'
r 📖	CompOp	7 math math: one_rel, r_eq_r', r_of_eq, r_iff_exists, Submonoid.LocalizationMap.eq', r_iff_oreEqv_r, mk_eq_mk_iff
r' 📖	CompOp	1 math math: r_eq_r'
rec 📖	CompOp	—
recOnSubsingleton₂ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind 📖	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	—	mk_eq_mk_iff
induction_on 📖	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	—	ind
induction_on₂ 📖	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	—	induction_on
induction_on₃ 📖	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	—	induction_on₂ induction_on
instIsMulTorsionFree 📖	mathematical	—	IsMulTorsionFree Localization OreLocalization.instMonoid CommMonoid.toMonoid OreLocalization.oreSetComm	—	Submonoid.instSubmonoidClass mk_pow pow_left_injective pow_zero mul_pow pow_succ mul_assoc
instSMulCommClassOfIsScalarTower 📖	mathematical	—	SMulCommClass SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	one_smul smul_assoc SMulCommClass.smul_comm smulCommClass_self
liftOn_mk 📖	mathematical	—	liftOn	—	—
liftOn_mk' 📖	mathematical	—	liftOn Submonoid.LocalizationMap.mk' Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm monoidOf	—	mk_eq_monoidOf_mk'
liftOn₂_mk 📖	mathematical	—	liftOn₂	—	—
liftOn₂_mk' 📖	mathematical	—	liftOn₂ Submonoid.LocalizationMap.mk' Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm monoidOf	—	mk_eq_monoidOf_mk'
mkHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Localization MulOneClass.toMulOne Prod.instMulOneClass Submonoid.toMulOneClass OreLocalization.instMonoid OreLocalization.oreSetComm MonoidHom.instFunLike mkHom	—	—
mkHom_surjective 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Localization DFunLike.coe MonoidHom MulOneClass.toMulOne Prod.instMulOneClass Submonoid.toMulOneClass OreLocalization.instMonoid OreLocalization.oreSetComm MonoidHom.instFunLike mkHom	—	—
mk_eq_mk_iff 📖	mathematical	—	DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp r	—	—
mk_eq_mk_iff' 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	IsCancelMul.toIsLeftCancelMul One.instNonempty
mk_eq_monoidOf_mk' 📖	mathematical	—	Submonoid.LocalizationMap.mk' Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm monoidOf	—	mk_eq_monoidOf_mk'_apply
mk_eq_monoidOf_mk'_apply 📖	mathematical	—	Submonoid.LocalizationMap.mk' Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm monoidOf	—	Submonoid.LocalizationMap.map_units Submonoid.instSubmonoidClass Submonoid.LocalizationMap.mul_inv_right mk_mul SubmonoidClass.toMulMemClass mul_comm mul_one mk_eq_mk_iff Con.symm Con.mul Con.refl one_rel
mk_left_injective 📖	mathematical	—	Localization	—	IsCancelMul.toIsLeftCancelMul One.instNonempty
mk_mul 📖	mathematical	—	Localization OreLocalization.instMul CommMonoid.toMonoid OreLocalization.oreSetComm MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Submonoid SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass OreLocalization.oreDiv_mul_oreDiv mul_comm
mk_one 📖	mathematical	—	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one Localization OreLocalization.instOne OreLocalization.oreSetComm Monoid.toMulAction	—	OreLocalization.one_def
mk_one_eq_monoidOf_mk 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one DFunLike.coe Submonoid.LocalizationMap Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm Submonoid.LocalizationMap.instFunLike monoidOf	—	—
mk_pow 📖	mathematical	—	Localization Monoid.toNatPow OreLocalization.instMonoid CommMonoid.toMonoid OreLocalization.oreSetComm Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike SubmonoidClass.nPow Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass pow_zero pow_succ
mk_prod 📖	mathematical	—	Finset.prod Localization OreLocalization.instCommMonoid OreLocalization.oreSetComm Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.toCommMonoid	—	Finset.induction_on mk_one Finset.prod_insert mk_mul
mk_self 📖	mathematical	—	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Localization OreLocalization.instOne OreLocalization.oreSetComm Monoid.toMulAction MulOne.toOne MulOneClass.toMulOne	—	mk_one mk_eq_mk_iff one_rel
mk_self_mk 📖	mathematical	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	Localization OreLocalization.instOne OreLocalization.oreSetComm Monoid.toMulAction MulOne.toOne MulOneClass.toMulOne	—	mk_self
ndrec_mk 📖	—	Localization DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp r mk_eq_mk_iff	—	—	mk_eq_mk_iff
one_rel 📖	mathematical	—	DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp r Prod.instOne MulOne.toOne Submonoid.one	—	—
r_eq_r' 📖	mathematical	—	r r'	—	le_antisymm sInf_le mul_one one_mul le_sInf Con.trans Con.mul Con.refl SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_assoc mul_comm Con.symm
r_iff_exists 📖	mathematical	—	DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp r	—	r_eq_r'
r_iff_oreEqv_r 📖	mathematical	—	DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp r OreLocalization.oreEqv OreLocalization.oreSetComm Monoid.toMulAction	—	MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_assoc mul_right_comm mul_comm
r_of_eq 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	DFunLike.coe Con Prod.instMul Submonoid.mul Con.instFunLikeForallProp r	—	r_iff_exists
smul_mk 📖	mathematical	—	Localization OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid OreLocalization.oreSetComm Monoid.toMulAction	—	OreLocalization.smul_one_oreDiv_one_smul OreLocalization.oreDiv_smul_oreDiv smul_assoc one_smul mul_one

MonoidHom

Definitions

Name	Category	Theorems
toLocalizationMap 📖	CompOp	—

OreLocalization

Definitions

Name	Category	Theorems
equivMonoidLocalization 📖	CompOp	—
localizationMap 📖	CompOp	—

Submonoid

Definitions

Name	Category	Theorems
IsLocalizationMap 📖	CompData	7 math math: LocalizationMap.isLocalizationMap, IsLocalization'.toIsLocalizationMap, isLocalizationMap_iff, isLocalizationMap_iff_bijective, isLocalizationMap_id, isLocalizationMap_of_group, isLocalization_iff_isLocalizationMap
LocalizationMap 📖	CompData	55 math math: LocalizationMap.injective_iff, LocalizationMap.mul_mk'_eq_mk'_of_mul, Localization.mulEquivOfQuotient_symm_monoidOf, LocalizationMap.map_spec, LocalizationMap.ofMulEquivOfDom_comp_symm, LocalizationMap.mk'_one, LocalizationMap.top_injective_iff, Localization.mk_one_eq_monoidOf_mk, LocalizationMap.mk'_eq_iff_eq, LocalizationMap.nonZeroDivisors_le_comap, LocalizationMap.eq_iff_exists, IsLocalization.toLocalizationMap_apply, LocalizationMap.mk'_mul_cancel_left, LocalizationMap.map_eq_zero_iff, LocalizationMap.ofMulEquivOfDom_comp, LocalizationMap.ext_iff, LocalizationMap.instMonoidHomClass, LocalizationMap.map_nonZeroDivisors_le, IsLocalization.coe_toLocalizationMap, Localization.monoidOf_eq_algebraMap, LocalizationMap.mk'_eq_iff_eq', LocalizationMap.sec_spec', LocalizationMap.mk'_mul_eq_mk'_of_mul, LocalizationMap.map_zero, instMonoidWithZeroHomClassLocalizationMap, LocalizationMap.of_mulEquivOfMulEquiv_apply, LocalizationMap.map_eq, mem_divPairs, LocalizationMap.mk'_mul_cancel_right, LocalizationMap.mk'_spec', LocalizationMap.ofMulEquivOfLocalizations_apply, Localization.mulEquivOfQuotient_monoidOf, LocalizationMap.mul_mk'_one_eq_mk', LocalizationMap.ofMulEquivOfDom_apply, LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq, LocalizationMap.map_mul_left, LocalizationMap.lift_eq, LocalizationMap.eq_mk'_iff_mul_eq, LocalizationMap.map_units, LocalizationMap.mulEquivOfMulEquiv_eq, LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply, LocalizationMap.surj, LocalizationMap.mulEquivOfLocalizations_right_inv_apply, LocalizationMap.mk'_eq_iff_eq_mul, LocalizationMap.toMonoidHom_apply, LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply', LocalizationMap.lift_injective_iff, LocalizationMap.sec_spec, LocalizationMap.map_isRegular, LocalizationMap.mk'_spec, LocalizationMap.map_mul_right, LocalizationMap.sec_zero_fst, LocalizationMap.toMonoidHom_injective, LocalizationMap.eq_iff_eq, LocalizationMap.surj₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalizationMap_id 📖	mathematical	—	IsLocalizationMap CommGroup.toCommMonoid	—	isLocalizationMap_iff_bijective MulHom.mulHomClass Function.bijective_id
isLocalizationMap_iff 📖	mathematical	—	IsLocalizationMap IsUnit CommMonoid.toMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership instSetLike MulOne.toMul MulOneClass.toMulOne	—	—
isLocalizationMap_iff_bijective 📖	mathematical	—	IsLocalizationMap CommGroup.toCommMonoid DFunLike.coe Function.Bijective	—	IsLocalizationMap.exists_of_eq mul_left_cancel LeftCancelSemigroup.toIsLeftCancelMul IsLocalizationMap.surj div_eq_mul_inv map_mul mul_assoc mul_inv_cancel IsLocalizationMap.map_one mul_one IsUnit.map MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Group.isUnit MulEquiv.map_one One.instNonempty
isLocalizationMap_of_group 📖	mathematical	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup	IsLocalizationMap CommGroup.toCommMonoid	—	Group.isUnit div_mul_cancel One.instNonempty

Submonoid.IsLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_of_eq 📖	mathematical	Submonoid.IsLocalizationMap	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	—
map_one 📖	mathematical	Submonoid.IsLocalizationMap DFunLike.coe	MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	map_units mul_one map_mul
map_units 📖	mathematical	Submonoid.IsLocalizationMap	IsUnit CommMonoid.toMonoid Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike	—	—
mulEquiv_comp 📖	mathematical	Submonoid.IsLocalizationMap	DFunLike.coe EquivLike.toFunLike	—	IsUnit.map MulEquivClass.instMonoidHomClass map_units surj MulEquiv.injective map_mul MonoidHomClass.toMulHomClass MulEquiv.instMulEquivClass MulEquivClass.coe_symm_apply_apply exists_of_eq EquivLike.injective
surj 📖	mathematical	Submonoid.IsLocalizationMap	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	—

Submonoid.LocalizationMap

Definitions

Name	Category	Theorems
instFunLike 📖	CompOp	56 math math: injective_iff, mul_mk'_eq_mk'_of_mul, Localization.mulEquivOfQuotient_symm_monoidOf, AwayMap.lift_comp, map_spec, ofMulEquivOfDom_comp_symm, mk'_one, top_injective_iff, Localization.mk_one_eq_monoidOf_mk, mk'_eq_iff_eq, nonZeroDivisors_le_comap, AwayMap.lift_eq, eq_iff_exists, IsLocalization.toLocalizationMap_apply, mk'_mul_cancel_left, map_eq_zero_iff, ofMulEquivOfDom_comp, ext_iff, instMonoidHomClass, map_nonZeroDivisors_le, IsLocalization.coe_toLocalizationMap, Localization.monoidOf_eq_algebraMap, mk'_eq_iff_eq', sec_spec', mk'_mul_eq_mk'_of_mul, map_zero, Submonoid.instMonoidWithZeroHomClassLocalizationMap, of_mulEquivOfMulEquiv_apply, map_eq, Submonoid.mem_divPairs, mk'_mul_cancel_right, mk'_spec', ofMulEquivOfLocalizations_apply, Localization.mulEquivOfQuotient_monoidOf, mul_mk'_one_eq_mk', ofMulEquivOfDom_apply, ofMulEquivOfLocalizations_eq_iff_eq, map_mul_left, lift_eq, eq_mk'_iff_mul_eq, map_units, mulEquivOfMulEquiv_eq, symm_comp_ofMulEquivOfLocalizations_apply, surj, mulEquivOfLocalizations_right_inv_apply, mk'_eq_iff_eq_mul, toMonoidHom_apply, symm_comp_ofMulEquivOfLocalizations_apply', lift_injective_iff, sec_spec, map_isRegular, mk'_spec, map_mul_right, sec_zero_fst, eq_iff_eq, surj₂
mk' 📖	CompOp	42 math math: Localization.Away.mk_eq_monoidOf_mk', Localization.mk_eq_monoidOf_mk', lift_eq_iff, mul_mk'_eq_mk'_of_mul, mk'_zero, mk'_eq_iff_mk'_eq, mk'_self, lift_localizationMap_mk', mk'_one, Localization.liftOn₂_mk', mk'_eq_of_eq, mk'_eq_iff_eq, map_mk', Localization.mulEquivOfQuotient_mk, mk'_eq_of_same, Localization.mk_eq_monoidOf_mk'_apply, mk'_mul_cancel_left, mk'_cancel, Localization.mulEquivOfQuotient_mk', lift_mk', exists_of_sec_mk', Localization.mulEquivOfQuotient_symm_mk, mk'_eq_iff_eq', mk'_mul_eq_mk'_of_mul, eq', mk'_mul_cancel_right, mk'_spec', mk'_eq_of_eq', mul_mk'_one_eq_mk', mk'_mul, mulEquivOfMulEquiv_mk', mk'_eq_zero_iff, eq_mk'_iff_mul_eq, lift_mk'_spec, mk'_self', Localization.liftOn_mk', mk'_sec, mk'_surjective, Localization.mulEquivOfQuotient_symm_mk', mk'_eq_iff_eq_mul, mk'_spec, eq
sec 📖	CompOp	17 math math: lift_spec, lift_mul_right, IsLocalization.lift_spec_mul_add, map_spec, exists_of_sec_mk', IsLocalization.toLocalizationMap_sec, sec_spec', lift_apply, map_mul_left, lift_spec_mul, lift_mul_left, Algebra.GrothendieckGroup.lift_apply, lift₀_apply, mk'_sec, sec_spec, map_mul_right, sec_zero_fst
toMonoidHom 📖	CompOp	19 math math: lift_comp_lift_eq, mulEquivOfLocalizations_apply, lift_of_comp, ofMulEquivOfLocalizations_comp, lift_localizationMap_mk', isUnit_comp, lift_comp, mulEquivOfLocalizations_symm_apply, IsLocalization.toLocalizationMap_toMonoidHom, of_mulEquivOfMulEquiv, Localization.mulEquivOfQuotient_apply, lift_left_inverse, map_comp, ofMulEquivOfLocalizations_eq, toMonoidHom_apply, ofMulEquivOfDom_eq, lift_comp_lift, toMonoidHom_injective, lift_id
toMulHom 📖	CompOp	1 math math: isLocalizationMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epic_of_localizationMap 📖	—	MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid toMonoidHom	—	—	MonoidHom.ext surj IsUnit.map MonoidHom.instMonoidHomClass map_units MonoidHom.map_mul
eq 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	mk'_eq_iff_eq eq_iff_exists
eq' 📖	mathematical	—	mk' DFunLike.coe Con Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Prod.instMul MulOne.toMul MulOneClass.toMulOne Submonoid.mul Con.instFunLikeForallProp Localization.r	—	eq Localization.r_iff_exists
eq_iff_eq 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap instFunLike	—	eq_iff_exists
eq_iff_exists 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.exists_of_eq isLocalizationMap map_units map_mul MonoidHomClass.toMulHomClass instMonoidHomClass
eq_mk'_iff_mul_eq 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	—	mk'_spec map_units mk'.eq_1 Submonoid.instSubmonoidClass mul_inv_right
exists_of_eq 📖	mathematical	DFunLike.coe Submonoid.LocalizationMap instFunLike	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.exists_of_eq isLocalizationMap
exists_of_sec_mk' 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike sec mk'	—	eq_iff_exists mk'_eq_iff_eq mk'_sec
ext 📖	—	DFunLike.coe Submonoid.LocalizationMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap instFunLike	—	ext
injective_iff 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap instFunLike IsRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Commute.isRegular_iff Commute.all forall₂_swap
instIsCancelMulLocalization 📖	mathematical	—	IsCancelMul Localization OreLocalization.instMul CommMonoid.toMonoid OreLocalization.oreSetComm	—	isCancelMul
instMonoidHomClass 📖	mathematical	—	MonoidHomClass Submonoid.LocalizationMap MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instFunLike	—	MulHom.map_mul MonoidHom.map_one
instNontrivialLocalizationOfIsCancelMul 📖	mathematical	—	Nontrivial Localization	—	Function.Injective.nontrivial injective_iff IsRegular.all
instSubsingletonLocalization 📖	mathematical	—	Localization	—	subsingleton_of_subsingleton
inv_inj 📖	—	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike Units Units.instInv Submonoid.toMonoid Units.instMulOneClass IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass	—	—	Submonoid.instSubmonoidClass mul_one mul_inv_left Units.inv_mul
inv_unique 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike MulOne.toMul MulOne.toOne	Units.val Units Units.instInv Submonoid.toMonoid Units.instMulOneClass IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass one_mul Units.val_mul mul_inv_left
isCancelMul 📖	mathematical	—	IsCancelMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Commute.isRegular_iff Commute.all Commute.isRightRegular_iff surj IsRightRegular.of_mul IsRegular.right map_isRegular isCancelMul_iff_forall_isRegular
isLocalizationMap 📖	mathematical	—	Submonoid.IsLocalizationMap MulHom.toFun MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid toMulHom	—	—
isUnit_comp 📖	mathematical	—	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike MonoidHom.comp toMonoidHom Submonoid SetLike.instMembership Submonoid.instSetLike	—	Submonoid.instSubmonoidClass map_units IsUnit.coe_liftRight
map_isRegular 📖	mathematical	IsRegular MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	DFunLike.coe Submonoid.LocalizationMap instFunLike	—	Commute.isRegular_iff Commute.all surj map_units Submonoid.coe_mul map_mul MonoidHomClass.toMulHomClass instMonoidHomClass mul_assoc mul_right_comm IsRegular.left mul_left_comm
map_left_cancel 📖	—	DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	—	map_right_cancel mul_comm
map_right_cancel 📖	—	DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	—	map_units map_mul MonoidHomClass.toMulHomClass instMonoidHomClass
map_units 📖	mathematical	—	IsUnit CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.map_units isLocalizationMap
mk'_cancel 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	mk'_eq_of_eq' Submonoid.coe_mul mul_comm mul_assoc
mk'_eq_iff_eq 📖	mathematical	—	mk' DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	map_mul MonoidHomClass.toMulHomClass instMonoidHomClass mk'_eq_iff_eq_mul mul_assoc mk'_spec' mul_comm map_units mk'.eq_1 Submonoid.instSubmonoidClass mul_inv_right toMonoidHom_apply
mk'_eq_iff_eq' 📖	mathematical	—	mk' DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	mk'_eq_iff_eq mul_comm
mk'_eq_iff_eq_mul 📖	mathematical	—	mk' DFunLike.coe Submonoid.LocalizationMap instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	eq_mk'_iff_mul_eq
mk'_eq_iff_mk'_eq 📖	mathematical	—	mk'	—	eq'
mk'_eq_of_eq 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	mk'	—	mk'_eq_iff_eq
mk'_eq_of_eq' 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	mk'	—	mk'_eq_of_eq mul_comm
mk'_eq_of_same 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike	—	mk'_eq_iff_eq' map_mul MonoidHomClass.toMulHomClass instMonoidHomClass eq_iff_exists map_units
mk'_mul 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike Submonoid.mul	—	Submonoid.instSubmonoidClass map_units mul_inv_left map_mul MonoidHomClass.toMulHomClass instMonoidHomClass MonoidHom.instMonoidHomClass mul_mul_mul_comm mul_left_comm IsUnit.mul_val_inv mul_one
mk'_mul_cancel_left 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike DFunLike.coe Submonoid.LocalizationMap instFunLike	—	mul_comm mk'_mul_cancel_right
mk'_mul_cancel_right 📖	mathematical	—	mk' MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Submonoid SetLike.instMembership Submonoid.instSetLike DFunLike.coe Submonoid.LocalizationMap instFunLike	—	mul_mk'_one_eq_mk' map_mul MonoidHomClass.toMulHomClass instMonoidHomClass mul_assoc mk'_self' mul_one
mk'_mul_eq_mk'_of_mul 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid mk' DFunLike.coe Submonoid.LocalizationMap instFunLike	—	mul_comm mul_mk'_eq_mk'_of_mul
mk'_one 📖	mathematical	—	mk' Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.one DFunLike.coe Submonoid.LocalizationMap instFunLike	—	map_units mk'.eq_1 map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one
mk'_sec 📖	mathematical	—	mk' Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike sec	—	map_units sec_spec Submonoid.instSubmonoidClass mul_inv_left mul_comm
mk'_self 📖	mathematical	Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	mk' MulOne.toOne MulOneClass.toMulOne	—	mk'_self'
mk'_self' 📖	mathematical	—	mk' Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike MulOne.toOne MulOneClass.toMulOne	—	map_units Submonoid.instSubmonoidClass mul_inv_left mul_one
mk'_spec 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid mk' DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	—	map_units mul_assoc mul_comm Submonoid.instSubmonoidClass mul_inv_left
mk'_spec' 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike mk'	—	mul_comm mk'_spec
mk'_surjective 📖	mathematical	—	mk'	—	mk'_sec
mul_inv 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	MulOne.toMul Units.val Units Units.instInv Submonoid.toMonoid Units.instMulOneClass IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass mul_inv_right mul_assoc mul_comm mul_inv_left MonoidHom.map_mul
mul_inv_left 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	MulOne.toMul Units.val Units Units.instInv Submonoid.toMonoid Units.instMulOneClass IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass mul_comm Units.inv_mul_eq_iff_eq_mul
mul_inv_right 📖	mathematical	IsUnit CommMonoid.toMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	MulOne.toMul Units.val Units Units.instInv Submonoid.toMonoid Units.instMulOneClass IsUnit.liftRight MonoidHom.restrict Submonoid.instSubmonoidClass	—	Submonoid.instSubmonoidClass mul_inv_left mul_comm
mul_mk'_eq_mk'_of_mul 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike mk'	—	mk'_one mk'_mul one_mul
mul_mk'_one_eq_mk' 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike mk' MulOne.toOne	—	mul_mk'_eq_mk'_of_mul mul_one
sec_spec 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike sec	—	surj
sec_spec' 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike sec MulOne.toMul MulOneClass.toMulOne	—	mul_comm sec_spec
subsingleton_of_subsingleton 📖	—	—	—	—	mk'_surjective instSubsingletonSubtype_mathlib
surj 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	—	Submonoid.IsLocalizationMap.surj isLocalizationMap
surj₂ 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid DFunLike.coe Submonoid.LocalizationMap instFunLike Submonoid SetLike.instMembership Submonoid.instSetLike	—	surj map_mul MonoidHomClass.toMulHomClass instMonoidHomClass mul_assoc mul_left_comm
toMonoidHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MonoidHom.instFunLike toMonoidHom Submonoid.LocalizationMap instFunLike	—	—
toMonoidHom_injective 📖	mathematical	—	Submonoid.LocalizationMap MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid toMonoidHom	—	MulHom.ext isLocalizationMap
top_injective_iff 📖	mathematical	—	DFunLike.coe Submonoid.LocalizationMap Top.top Submonoid Monoid.toMulOneClass CommMonoid.toMonoid Submonoid.instTop instFunLike IsCancelMul MulOne.toMul MulOneClass.toMulOne	—	—

(root)

Definitions

Name	Category	Theorems
AddLocalization 📖	CompOp	33 math math: AddLocalization.isOrderedAddCancelMonoid, AddLocalization.liftOn_mk', AddLocalization.mk_left_injective, AddLocalization.mkOrderEmbedding_apply, AddLocalization.cardinalMk_le, AddLocalization.mk_self, Algebra.GrothendieckAddGroup.neg_mk, AddLocalization.mk_self_mk, AddLocalization.fg, AddLocalization.mk_zero_eq_addMonoidOf_mk, AddLocalization.addEquivOfQuotient_mk', AddLocalization.mk_eq_addMonoidOf_mk', AddLocalization.mk_le_mk, AddLocalization.addEquivOfQuotient_apply, AddSubmonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelAdd, AddLocalization.addEquivOfQuotient_mk, AddLocalization.addEquivOfQuotient_symm_mk', AddLocalization.mk_add, AddLocalization.mk_zero, AddLocalization.mk_lt_mk, AddLocalization.mkHom_apply, AddLocalization.mkHom_surjective, AddLocalization.instIsAddTorsionFree, AddLocalization.mk_sum, AddLocalization.liftOn₂_mk', AddLocalization.addEquivOfQuotient_symm_mk, Algebra.GrothendieckAddGroup.lift_apply, AddLocalization.addEquivOfQuotient_addMonoidOf, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, AddLocalization.mk_nsmul, AddSubmonoid.LocalizationMap.instIsCancelAddLocalization, AddLocalization.mk_eq_addMonoidOf_mk'_apply, Algebra.GrothendieckAddGroup.mk_sub_mk

---

← Back to Index