Maps

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

Statistics

Metric	Count
Definitions `addEquivOfQuotient`, `addEquivOfAddEquiv`, `addEquivOfLocalizations`, `map`, `ofAddEquivOfDom`, `ofAddEquivOfLocalizations`, `mulEquivOfQuotient`, `map`, `mulEquivOfLocalizations`, `mulEquivOfMulEquiv`, `ofMulEquivOfDom`, `ofMulEquivOfLocalizations`	12
Theorems `addEquivOfQuotient_addMonoidOf`, `addEquivOfQuotient_apply`, `addEquivOfQuotient_mk`, `addEquivOfQuotient_mk'`, `addEquivOfQuotient_symm_addMonoidOf`, `addEquivOfQuotient_symm_mk`, `addEquivOfQuotient_symm_mk'`, `addEquivOfAddEquiv_eq`, `addEquivOfAddEquiv_eq_map`, `addEquivOfAddEquiv_eq_map_apply`, `addEquivOfAddEquiv_mk'`, `addEquivOfLocalizations_apply`, `addEquivOfLocalizations_left_neg`, `addEquivOfLocalizations_left_neg_apply`, `addEquivOfLocalizations_right_inv`, `addEquivOfLocalizations_right_inv_apply`, `addEquivOfLocalizations_symm_apply`, `addEquivOfLocalizations_symm_eq_addEquivOfLocalizations`, `comp_eq_of_eq`, `eq_of_eq`, `lift_add_left`, `lift_add_right`, `lift_apply`, `lift_comp`, `lift_comp_lift`, `lift_comp_lift_eq`, `lift_eq`, `lift_eq_iff`, `lift_id`, `lift_injective_iff`, `lift_left_inverse`, `lift_localizationMap_mk'`, `lift_mk'`, `lift_mk'_spec`, `lift_of_comp`, `lift_spec`, `lift_spec_add`, `lift_surjective_iff`, `lift_unique`, `map_add_left`, `map_add_right`, `map_comp`, `map_comp_map`, `map_eq`, `map_id`, `map_injective_of_injective`, `map_injective_of_surjOn_or_injective`, `map_map`, `map_mk'`, `map_spec`, `map_surjective_of_surjOn`, `map_surjective_of_surjective`, `ofAddEquivOfDom_apply`, `ofAddEquivOfDom_comp`, `ofAddEquivOfDom_comp_symm`, `ofAddEquivOfDom_eq`, `ofAddEquivOfDom_id`, `ofAddEquivOfLocalizations_apply`, `ofAddEquivOfLocalizations_comp`, `ofAddEquivOfLocalizations_eq`, `ofAddEquivOfLocalizations_eq_iff_eq`, `ofAddEquivOfLocalizations_id`, `of_addEquivOfAddEquiv`, `of_addEquivOfAddEquiv_apply`, `symm_comp_ofAddEquivOfLocalizations_apply`, `symm_comp_ofAddEquivOfLocalizations_apply'`, `mulEquivOfQuotient_apply`, `mulEquivOfQuotient_mk`, `mulEquivOfQuotient_mk'`, `mulEquivOfQuotient_monoidOf`, `mulEquivOfQuotient_symm_mk`, `mulEquivOfQuotient_symm_mk'`, `mulEquivOfQuotient_symm_monoidOf`, `comp_eq_of_eq`, `eq_of_eq`, `lift_apply`, `lift_comp`, `lift_comp_lift`, `lift_comp_lift_eq`, `lift_eq`, `lift_eq_iff`, `lift_id`, `lift_injective_iff`, `lift_left_inverse`, `lift_localizationMap_mk'`, `lift_mk'`, `lift_mk'_spec`, `lift_mul_left`, `lift_mul_right`, `lift_of_comp`, `lift_spec`, `lift_spec_mul`, `lift_surjective_iff`, `lift_unique`, `map_comp`, `map_comp_map`, `map_eq`, `map_id`, `map_injective_of_injective`, `map_injective_of_surjOn_or_injective`, `map_map`, `map_mk'`, `map_mul_left`, `map_mul_right`, `map_spec`, `map_surjective_of_surjOn`, `map_surjective_of_surjective`, `mulEquivOfLocalizations_apply`, `mulEquivOfLocalizations_left_inv`, `mulEquivOfLocalizations_left_inv_apply`, `mulEquivOfLocalizations_right_inv`, `mulEquivOfLocalizations_right_inv_apply`, `mulEquivOfLocalizations_symm_apply`, `mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations`, `mulEquivOfMulEquiv_eq`, `mulEquivOfMulEquiv_eq_map`, `mulEquivOfMulEquiv_eq_map_apply`, `mulEquivOfMulEquiv_mk'`, `ofMulEquivOfDom_apply`, `ofMulEquivOfDom_comp`, `ofMulEquivOfDom_comp_symm`, `ofMulEquivOfDom_eq`, `ofMulEquivOfDom_id`, `ofMulEquivOfLocalizations_apply`, `ofMulEquivOfLocalizations_comp`, `ofMulEquivOfLocalizations_eq`, `ofMulEquivOfLocalizations_eq_iff_eq`, `ofMulEquivOfLocalizations_id`, `of_mulEquivOfMulEquiv`, `of_mulEquivOfMulEquiv_apply`, `symm_comp_ofMulEquivOfLocalizations_apply`, `symm_comp_ofMulEquivOfLocalizations_apply'`	132
Total	144

AddLocalization

Definitions

Name	Category	Theorems
`addEquivOfQuotient` 📖	CompOp	7 math math: `addEquivOfQuotient_mk'`, `addEquivOfQuotient_apply`, `addEquivOfQuotient_mk`, `addEquivOfQuotient_symm_mk'`, `addEquivOfQuotient_symm_mk`, `addEquivOfQuotient_addMonoidOf`, `addEquivOfQuotient_symm_addMonoidOf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquivOfQuotient_addMonoidOf` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddOreLocalization.instAdd` `AddCommMonoid.toAddMonoid` `AddOreLocalization.addOreSetComm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap` `AddOreLocalization.instAddCommMonoid` `AddSubmonoid.LocalizationMap.instFunLike` `addMonoidOf`	—	`AddSubmonoid.LocalizationMap.lift_eq` `AddSubmonoid.LocalizationMap.map_addUnits`
`addEquivOfQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddOreLocalization.instAdd` `AddCommMonoid.toAddMonoid` `AddOreLocalization.addOreSetComm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfQuotient` `AddMonoidHom` `AddOreLocalization.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddSubmonoid.LocalizationMap.lift` `addMonoidOf` `AddSubmonoid.LocalizationMap.toAddMonoidHom` `AddSubmonoid.LocalizationMap.map_addUnits`	—	—
`addEquivOfQuotient_mk` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddOreLocalization.instAdd` `AddCommMonoid.toAddMonoid` `AddOreLocalization.addOreSetComm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap.mk'`	—	`mk_eq_addMonoidOf_mk'_apply` `addEquivOfQuotient_mk'`
`addEquivOfQuotient_mk'` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddOreLocalization.instAdd` `AddCommMonoid.toAddMonoid` `AddOreLocalization.addOreSetComm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap.mk'` `AddOreLocalization.instAddCommMonoid` `addMonoidOf`	—	`AddSubmonoid.LocalizationMap.lift_mk'` `AddSubmonoid.LocalizationMap.map_addUnits`
`addEquivOfQuotient_symm_addMonoidOf` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddOreLocalization.instAdd` `AddOreLocalization.addOreSetComm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap` `AddSubmonoid.LocalizationMap.instFunLike` `AddOreLocalization.instAddCommMonoid` `addMonoidOf`	—	`AddSubmonoid.LocalizationMap.lift_eq` `AddSubmonoid.LocalizationMap.map_addUnits`
`addEquivOfQuotient_symm_mk` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddOreLocalization.instAdd` `AddOreLocalization.addOreSetComm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap.mk'`	—	`mk_eq_addMonoidOf_mk'_apply` `addEquivOfQuotient_symm_mk'`
`addEquivOfQuotient_symm_mk'` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddLocalization` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddOreLocalization.instAdd` `AddOreLocalization.addOreSetComm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOfQuotient` `AddSubmonoid.LocalizationMap.mk'` `AddOreLocalization.instAddCommMonoid` `addMonoidOf`	—	`AddSubmonoid.LocalizationMap.lift_mk'` `AddSubmonoid.LocalizationMap.map_addUnits`

AddSubmonoid.LocalizationMap

Definitions

Name	Category	Theorems
`addEquivOfAddEquiv` 📖	CompOp	6 math math: `addEquivOfAddEquiv_eq`, `addEquivOfAddEquiv_mk'`, `of_addEquivOfAddEquiv_apply`, `addEquivOfAddEquiv_eq_map_apply`, `addEquivOfAddEquiv_eq_map`, `of_addEquivOfAddEquiv`
`addEquivOfLocalizations` 📖	CompOp	8 math math: `addEquivOfLocalizations_symm_apply`, `AddSubmonoid.subPairs_comap`, `addEquivOfLocalizations_left_neg`, `addEquivOfLocalizations_right_inv_apply`, `addEquivOfLocalizations_symm_eq_addEquivOfLocalizations`, `addEquivOfLocalizations_left_neg_apply`, `addEquivOfLocalizations_right_inv`, `addEquivOfLocalizations_apply`
`map` 📖	CompOp	15 math math: `map_add_right`, `map_surjective_of_surjective`, `map_spec`, `map_add_left`, `addEquivOfAddEquiv_eq_map_apply`, `map_eq`, `map_comp`, `map_surjective_of_surjOn`, `map_injective_of_injective`, `map_comp_map`, `map_map`, `addEquivOfAddEquiv_eq_map`, `map_id`, `map_injective_of_surjOn_or_injective`, `map_mk'`
`ofAddEquivOfDom` 📖	CompOp	5 math math: `ofAddEquivOfDom_apply`, `ofAddEquivOfDom_id`, `ofAddEquivOfDom_eq`, `ofAddEquivOfDom_comp_symm`, `ofAddEquivOfDom_comp`
`ofAddEquivOfLocalizations` 📖	CompOp	13 math math: `ofAddEquivOfLocalizations_eq`, `symm_comp_ofAddEquivOfLocalizations_apply`, `ofAddEquivOfLocalizations_eq_iff_eq`, `of_addEquivOfAddEquiv_apply`, `symm_comp_ofAddEquivOfLocalizations_apply'`, `addEquivOfLocalizations_left_neg`, `ofAddEquivOfLocalizations_apply`, `addEquivOfLocalizations_right_inv_apply`, `ofAddEquivOfLocalizations_comp`, `addEquivOfLocalizations_left_neg_apply`, `of_addEquivOfAddEquiv`, `ofAddEquivOfLocalizations_id`, `addEquivOfLocalizations_right_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquivOfAddEquiv_eq` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfAddEquiv` `AddSubmonoid.LocalizationMap` `instFunLike`	—	`AddMonoidHom.instAddMonoidHomClass` `map_eq` `Set.mem_image_of_mem`
`addEquivOfAddEquiv_eq_map` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`addEquivOfAddEquiv` `map`	—	`AddMonoidHom.instAddMonoidHomClass`
`addEquivOfAddEquiv_eq_map_apply` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfAddEquiv` `map`	—	`AddMonoidHom.instAddMonoidHomClass`
`addEquivOfAddEquiv_mk'` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfAddEquiv` `mk'` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `Set.mem_image_of_mem` `SetLike.coe`	—	`AddMonoidHom.instAddMonoidHomClass` `map_mk'` `Set.mem_image_of_mem`
`addEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfLocalizations` `AddMonoidHom` `AddMonoidHom.instFunLike` `lift` `toAddMonoidHom` `map_addUnits`	—	—
`addEquivOfLocalizations_left_neg` 📖	mathematical	—	`addEquivOfLocalizations` `ofAddEquivOfLocalizations`	—	`DFunLike.ext` `isAddUnit_comp` `DFunLike.ext_iff` `lift_of_comp`
`addEquivOfLocalizations_left_neg_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquivOfLocalizations` `ofAddEquivOfLocalizations`	—	`addEquivOfLocalizations_left_neg`
`addEquivOfLocalizations_right_inv` 📖	mathematical	—	`ofAddEquivOfLocalizations` `addEquivOfLocalizations`	—	`toAddMonoidHom_injective` `lift_comp` `map_addUnits`
`addEquivOfLocalizations_right_inv_apply` 📖	mathematical	—	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations` `addEquivOfLocalizations`	—	`lift_eq` `map_addUnits`
`addEquivOfLocalizations_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquivOfLocalizations` `AddMonoidHom` `AddMonoidHom.instFunLike` `lift` `toAddMonoidHom` `map_addUnits`	—	—
`addEquivOfLocalizations_symm_eq_addEquivOfLocalizations` 📖	mathematical	—	`AddEquiv.symm` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addEquivOfLocalizations`	—	—
`comp_eq_of_eq` 📖	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddSubmonoid.LocalizationMap` `instFunLike`	—	—	`eq_of_eq` `map_addUnits`
`eq_of_eq` 📖	—	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.LocalizationMap` `instFunLike`	—	—	`eq_iff_exists` `zero_add` `AddSubmonoid.instAddSubmonoidClass` `IsAddUnit.liftRight_neg_add` `add_assoc` `AddMonoidHom.map_add` `add_comm` `add_neg_left`
`lift_add_left` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddZero.toAdd` `sec` `lift`	—	`add_comm` `lift_add_right`
`lift_add_right` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddZero.toAdd` `lift` `sec`	—	`AddSubmonoid.instAddSubmonoidClass` `lift_apply` `add_assoc` `AddMonoidHom.restrict_apply` `IsAddUnit.liftRight_neg_add` `add_zero`
`lift_apply` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `AddZero.toAdd` `sec` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `AddSubmonoid.toAddMonoid` `AddUnits.instAddZeroClass` `IsAddUnit.liftRight` `AddMonoidHom.restrict` `AddSubmonoid.instAddSubmonoidClass`	—	—
`lift_comp` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddMonoidHom.comp` `lift` `toAddMonoidHom`	—	`AddMonoidHom.ext` `lift_eq`
`lift_comp_lift` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubmonoid.instPartialOrder` `IsAddUnit` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddMonoidHom.comp` `lift` `toAddMonoidHom` `map_addUnits`	—	`map_addUnits` `lift_unique` `toAddMonoidHom_apply` `AddMonoidHom.comp_apply` `AddMonoidHom.comp_assoc` `lift_comp`
`lift_comp_lift_eq` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddMonoidHom.comp` `lift` `toAddMonoidHom` `map_addUnits`	—	`lift_comp_lift` `le_rfl`
`lift_eq` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `AddSubmonoid.LocalizationMap` `instFunLike`	—	`lift_spec` `AddMonoidHom.map_add` `eq_of_eq` `sec_spec'` `map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass`
`lift_eq_iff` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `mk'` `AddZero.toAdd`	—	`AddSubmonoid.instAddSubmonoidClass` `lift_mk'` `add_neg`
`lift_id` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `lift` `toAddMonoidHom` `map_addUnits`	—	`isAddUnit_comp` `DFunLike.ext_iff` `lift_of_comp`
`lift_injective_iff` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `AddSubmonoid.LocalizationMap` `instFunLike`	—	`eq_of_eq` `lift_eq` `surj` `mk'_sec` `AddSubmonoid.instAddSubmonoidClass` `map_addUnits` `add_neg`
`lift_left_inverse` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `lift` `toAddMonoidHom` `map_addUnits`	—	`map_addUnits` `DFunLike.congr_fun` `lift_comp_lift_eq` `lift_id`
`lift_localizationMap_mk'` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `lift` `toAddMonoidHom` `map_addUnits` `mk'`	—	`lift_mk'` `map_addUnits`
`lift_mk'` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `mk'` `AddZero.toAdd` `AddUnits.val` `AddUnits` `AddUnits.instNeg` `AddSubmonoid.toAddMonoid` `AddUnits.instAddZeroClass` `IsAddUnit.liftRight` `AddMonoidHom.restrict` `AddSubmonoid.instAddSubmonoidClass`	—	`AddSubmonoid.instAddSubmonoidClass` `add_neg` `eq_of_eq` `map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `sec_spec'` `add_assoc` `mk'_spec` `add_comm`
`lift_mk'_spec` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `mk'` `AddZero.toAdd`	—	`AddSubmonoid.instAddSubmonoidClass` `lift_mk'` `add_neg_left`
`lift_of_comp` 📖	mathematical	—	`lift` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `toAddMonoidHom` `isAddUnit_comp`	—	`AddMonoidHom.ext` `isAddUnit_comp` `lift_spec` `AddMonoidHom.comp_apply` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `sec_spec'`
`lift_spec` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `sec` `AddZero.toAdd`	—	`add_neg_left`
`lift_spec_add` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`AddZero.toAdd` `lift` `sec`	—	`add_comm` `AddSubmonoid.instAddSubmonoidClass` `lift_apply` `add_assoc` `add_neg_left`
`lift_surjective_iff` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	`lift` `AddZero.toAdd`	—	`surj` `eq_mk'_iff_add_eq` `AddSubmonoid.instAddSubmonoidClass` `lift_mk'` `add_assoc` `add_comm` `AddMonoidHom.restrict_apply` `IsAddUnit.add_liftRight_neg` `add_zero` `add_neg_left`
`lift_unique` 📖	mathematical	`IsAddUnit` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.LocalizationMap` `instFunLike`	`lift`	—	`AddMonoidHom.ext` `lift_spec` `AddMonoidHom.map_add` `sec_spec'`
`map_add_left` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `AddSubmonoid.LocalizationMap` `instFunLike` `sec` `map`	—	`add_comm` `map_add_right`
`map_add_right` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddZero.toAdd` `map` `AddSubmonoid.LocalizationMap` `instFunLike` `sec`	—	`lift_add_right` `map_addUnits`
`map_comp` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddMonoidHom.comp` `map` `toAddMonoidHom`	—	`lift_comp` `map_addUnits`
`map_comp_map` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`AddMonoidHom.comp` `map`	—	`AddMonoidHom.ext` `AddSubmonoid.instAddSubmonoidClass` `add_neg_left` `add_assoc` `add_neg_right` `map_add` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `AddMonoidHom.map_add` `comp_eq_of_eq` `sec_spec'` `map_add_right`
`map_eq` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`map` `AddSubmonoid.LocalizationMap` `instFunLike`	—	`lift_eq` `map_addUnits`
`map_id` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `map` `AddMonoidHom.id`	—	`lift_id`
`map_injective_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	`map` `AddSubmonoid.map` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.apply_coe_mem_map`	—	`AddMonoidHom.instAddMonoidHomClass` `map_injective_of_surjOn_or_injective` `AddSubmonoid.apply_coe_mem_map` `Set.surjOn_image`
`map_injective_of_surjOn_or_injective` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `Set.SurjOn` `SetLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike`	`map`	—	`map_eq` `surj₂` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `exists_of_eq` `map_addUnits` `eq_iff_exists` `IsAddUnit.add_right_cancel`
`map_map` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`map` `AddMonoidHom.comp`	—	`map_comp_map`
`map_mk'` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`map` `mk'`	—	`map.eq_1` `AddSubmonoid.instAddSubmonoidClass` `lift_mk'` `add_neg_left` `add_mk'_eq_mk'_of_add` `mk'_add_cancel_left`
`map_spec` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike`	`map` `AddSubmonoid.LocalizationMap` `instFunLike` `sec` `AddZero.toAdd`	—	`lift_spec` `map_addUnits`
`map_surjective_of_surjOn` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `Set.SurjOn` `SetLike.coe`	`map`	—	`mk'_surjective` `map_mk'`
`map_surjective_of_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	`map` `AddSubmonoid.map` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.apply_coe_mem_map`	—	`AddMonoidHom.instAddMonoidHomClass` `map_surjective_of_surjOn` `AddSubmonoid.apply_coe_mem_map` `Set.surjOn_image`
`ofAddEquivOfDom_apply` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfDom` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	`AddMonoidHom.instAddMonoidHomClass`
`ofAddEquivOfDom_comp` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom` `AddEquiv.symm` `AddZero.toAdd`	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfDom` `AddEquiv` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	`AddMonoidHom.instAddMonoidHomClass` `AddEquiv.symm_apply_apply`
`ofAddEquivOfDom_comp_symm` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfDom` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm`	—	`AddMonoidHom.instAddMonoidHomClass` `AddEquiv.apply_symm_apply`
`ofAddEquivOfDom_eq` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`toAddMonoidHom` `ofAddEquivOfDom` `AddMonoidHom.comp`	—	`AddMonoidHom.instAddMonoidHomClass`
`ofAddEquivOfDom_id` 📖	mathematical	—	`ofAddEquivOfDom` `AddEquiv.refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`ext` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.ext`
`ofAddEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	—
`ofAddEquivOfLocalizations_comp` 📖	mathematical	—	`toAddMonoidHom` `ofAddEquivOfLocalizations` `AddEquiv.trans` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.comp` `AddEquiv.toAddMonoidHom`	—	`AddMonoidHom.ext`
`ofAddEquivOfLocalizations_eq` 📖	mathematical	—	`toAddMonoidHom` `ofAddEquivOfLocalizations` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddEquiv.toAddMonoidHom`	—	—
`ofAddEquivOfLocalizations_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm`	—	`Equiv.eq_symm_apply`
`ofAddEquivOfLocalizations_id` 📖	mathematical	—	`ofAddEquivOfLocalizations` `AddEquiv.refl` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`ext`
`of_addEquivOfAddEquiv` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`toAddMonoidHom` `ofAddEquivOfLocalizations` `addEquivOfAddEquiv` `AddMonoidHom.comp`	—	`AddMonoidHom.instAddMonoidHomClass` `AddMonoidHom.ext` `of_addEquivOfAddEquiv_apply`
`of_addEquivOfAddEquiv_apply` 📖	mathematical	`AddSubmonoid.map` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `AddMonoidHom.instAddMonoidHomClass` `AddEquiv.toAddMonoidHom`	`DFunLike.coe` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations` `addEquivOfAddEquiv` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	`AddMonoidHom.instAddMonoidHomClass` `ext_iff` `addEquivOfLocalizations_right_inv`
`symm_comp_ofAddEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations`	—	`AddEquiv.symm_apply_apply`
`symm_comp_ofAddEquivOfLocalizations_apply'` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddSubmonoid.LocalizationMap` `instFunLike` `ofAddEquivOfLocalizations` `AddEquiv.symm`	—	`AddEquiv.apply_symm_apply`

Localization

Definitions

Name	Category	Theorems
`mulEquivOfQuotient` 📖	CompOp	7 math math: `mulEquivOfQuotient_symm_monoidOf`, `mulEquivOfQuotient_mk`, `mulEquivOfQuotient_mk'`, `mulEquivOfQuotient_symm_mk`, `mulEquivOfQuotient_monoidOf`, `mulEquivOfQuotient_apply`, `mulEquivOfQuotient_symm_mk'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulEquivOfQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `OreLocalization.instMul` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfQuotient` `MonoidHom` `OreLocalization.instCommMonoid` `MonoidHom.instFunLike` `Submonoid.LocalizationMap.lift` `monoidOf` `Submonoid.LocalizationMap.toMonoidHom` `Submonoid.LocalizationMap.map_units`	—	—
`mulEquivOfQuotient_mk` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `OreLocalization.instMul` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfQuotient` `Submonoid.LocalizationMap.mk'`	—	`mk_eq_monoidOf_mk'_apply` `mulEquivOfQuotient_mk'`
`mulEquivOfQuotient_mk'` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `OreLocalization.instMul` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfQuotient` `Submonoid.LocalizationMap.mk'` `OreLocalization.instCommMonoid` `monoidOf`	—	`Submonoid.LocalizationMap.lift_mk'` `Submonoid.LocalizationMap.map_units`
`mulEquivOfQuotient_monoidOf` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `OreLocalization.instMul` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfQuotient` `Submonoid.LocalizationMap` `OreLocalization.instCommMonoid` `Submonoid.LocalizationMap.instFunLike` `monoidOf`	—	`Submonoid.LocalizationMap.lift_eq` `Submonoid.LocalizationMap.map_units`
`mulEquivOfQuotient_symm_mk` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OreLocalization.instMul` `OreLocalization.oreSetComm` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquivOfQuotient` `Submonoid.LocalizationMap.mk'`	—	`mk_eq_monoidOf_mk'_apply` `mulEquivOfQuotient_symm_mk'`
`mulEquivOfQuotient_symm_mk'` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OreLocalization.instMul` `OreLocalization.oreSetComm` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquivOfQuotient` `Submonoid.LocalizationMap.mk'` `OreLocalization.instCommMonoid` `monoidOf`	—	`Submonoid.LocalizationMap.lift_mk'` `Submonoid.LocalizationMap.map_units`
`mulEquivOfQuotient_symm_monoidOf` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Localization` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `OreLocalization.instMul` `OreLocalization.oreSetComm` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquivOfQuotient` `Submonoid.LocalizationMap` `Submonoid.LocalizationMap.instFunLike` `OreLocalization.instCommMonoid` `monoidOf`	—	`Submonoid.LocalizationMap.lift_eq` `Submonoid.LocalizationMap.map_units`

Submonoid.LocalizationMap

Definitions

Name	Category	Theorems
`map` 📖	CompOp	15 math math: `map_id`, `map_injective_of_injective`, `map_spec`, `map_surjective_of_surjOn`, `map_surjective_of_surjective`, `map_comp_map`, `map_mk'`, `mulEquivOfMulEquiv_eq_map`, `map_eq`, `map_mul_left`, `map_comp`, `map_map`, `map_injective_of_surjOn_or_injective`, `map_mul_right`, `mulEquivOfMulEquiv_eq_map_apply`
`mulEquivOfLocalizations` 📖	CompOp	8 math math: `mulEquivOfLocalizations_apply`, `mulEquivOfLocalizations_symm_apply`, `mulEquivOfLocalizations_left_inv_apply`, `mulEquivOfLocalizations_left_inv`, `mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations`, `Submonoid.divPairs_comap`, `mulEquivOfLocalizations_right_inv`, `mulEquivOfLocalizations_right_inv_apply`
`mulEquivOfMulEquiv` 📖	CompOp	6 math math: `mulEquivOfMulEquiv_eq_map`, `of_mulEquivOfMulEquiv`, `of_mulEquivOfMulEquiv_apply`, `mulEquivOfMulEquiv_mk'`, `mulEquivOfMulEquiv_eq`, `mulEquivOfMulEquiv_eq_map_apply`
`ofMulEquivOfDom` 📖	CompOp	5 math math: `ofMulEquivOfDom_comp_symm`, `ofMulEquivOfDom_id`, `ofMulEquivOfDom_comp`, `ofMulEquivOfDom_apply`, `ofMulEquivOfDom_eq`
`ofMulEquivOfLocalizations` 📖	CompOp	13 math math: `ofMulEquivOfLocalizations_comp`, `ofMulEquivOfLocalizations_id`, `of_mulEquivOfMulEquiv`, `of_mulEquivOfMulEquiv_apply`, `ofMulEquivOfLocalizations_apply`, `mulEquivOfLocalizations_left_inv_apply`, `mulEquivOfLocalizations_left_inv`, `ofMulEquivOfLocalizations_eq_iff_eq`, `symm_comp_ofMulEquivOfLocalizations_apply`, `mulEquivOfLocalizations_right_inv`, `mulEquivOfLocalizations_right_inv_apply`, `ofMulEquivOfLocalizations_eq`, `symm_comp_ofMulEquivOfLocalizations_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_of_eq` 📖	—	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `Submonoid.LocalizationMap` `instFunLike`	—	—	`eq_of_eq` `map_units`
`eq_of_eq` 📖	—	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.LocalizationMap` `instFunLike`	—	—	`eq_iff_exists` `one_mul` `Submonoid.instSubmonoidClass` `IsUnit.liftRight_inv_mul` `mul_assoc` `MonoidHom.map_mul` `mul_comm` `mul_inv_left`
`lift_apply` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `MulOne.toMul` `sec` `Units.val` `Units` `Units.instInv` `Submonoid.toMonoid` `Units.instMulOneClass` `IsUnit.liftRight` `MonoidHom.restrict` `Submonoid.instSubmonoidClass`	—	—
`lift_comp` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`MonoidHom.comp` `lift` `toMonoidHom`	—	`MonoidHom.ext` `lift_eq`
`lift_comp_lift` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `IsUnit` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `SetLike.instMembership` `Submonoid.instSetLike`	`MonoidHom.comp` `lift` `toMonoidHom` `map_units`	—	`map_units` `lift_unique` `toMonoidHom_apply` `MonoidHom.comp_apply` `MonoidHom.comp_assoc` `lift_comp`
`lift_comp_lift_eq` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`MonoidHom.comp` `lift` `toMonoidHom` `map_units`	—	`lift_comp_lift` `le_rfl`
`lift_eq` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `Submonoid.LocalizationMap` `instFunLike`	—	`lift_spec` `MonoidHom.map_mul` `eq_of_eq` `sec_spec'` `map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass`
`lift_eq_iff` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `mk'` `MulOne.toMul`	—	`Submonoid.instSubmonoidClass` `lift_mk'` `mul_inv`
`lift_id` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `lift` `toMonoidHom` `map_units`	—	`isUnit_comp` `DFunLike.ext_iff` `lift_of_comp`
`lift_injective_iff` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `Submonoid.LocalizationMap` `instFunLike`	—	`eq_of_eq` `lift_eq` `surj` `mk'_sec` `Submonoid.instSubmonoidClass` `map_units` `mul_inv`
`lift_left_inverse` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `lift` `toMonoidHom` `map_units`	—	`map_units` `DFunLike.congr_fun` `lift_comp_lift_eq` `lift_id`
`lift_localizationMap_mk'` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `lift` `toMonoidHom` `map_units` `mk'`	—	`lift_mk'` `map_units`
`lift_mk'` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `mk'` `MulOne.toMul` `Units.val` `Units` `Units.instInv` `Submonoid.toMonoid` `Units.instMulOneClass` `IsUnit.liftRight` `MonoidHom.restrict` `Submonoid.instSubmonoidClass`	—	`Submonoid.instSubmonoidClass` `mul_inv` `eq_of_eq` `map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `sec_spec'` `mul_assoc` `mk'_spec` `mul_comm`
`lift_mk'_spec` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `mk'` `MulOne.toMul`	—	`Submonoid.instSubmonoidClass` `lift_mk'` `mul_inv_left`
`lift_mul_left` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`MulOne.toMul` `sec` `lift`	—	`mul_comm` `lift_mul_right`
`lift_mul_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`MulOne.toMul` `lift` `sec`	—	`Submonoid.instSubmonoidClass` `lift_apply` `mul_assoc` `MonoidHom.restrict_apply` `IsUnit.liftRight_inv_mul` `mul_one`
`lift_of_comp` 📖	mathematical	—	`lift` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `toMonoidHom` `isUnit_comp`	—	`MonoidHom.ext` `isUnit_comp` `MonoidHom.comp_apply` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `sec_spec'`
`lift_spec` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `sec` `MulOne.toMul`	—	`mul_inv_left`
`lift_spec_mul` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`MulOne.toMul` `lift` `sec`	—	`mul_comm` `Submonoid.instSubmonoidClass` `lift_apply` `mul_assoc` `mul_inv_left`
`lift_surjective_iff` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	`lift` `MulOne.toMul`	—	`surj` `eq_mk'_iff_mul_eq` `Submonoid.instSubmonoidClass` `lift_mk'` `mul_assoc` `mul_comm` `MonoidHom.restrict_apply` `IsUnit.mul_liftRight_inv` `mul_one` `mul_inv_left`
`lift_unique` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.LocalizationMap` `instFunLike`	`lift`	—	`MonoidHom.ext` `lift_spec` `MonoidHom.map_mul` `sec_spec'`
`map_comp` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MonoidHom.comp` `map` `toMonoidHom`	—	`lift_comp` `map_units`
`map_comp_map` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MonoidHom.comp` `map`	—	`MonoidHom.ext` `Submonoid.instSubmonoidClass` `mul_inv_left` `mul_assoc` `mul_inv_right` `map_mul` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `MonoidHom.map_mul` `comp_eq_of_eq` `sec_spec'` `map_mul_right`
`map_eq` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`map` `Submonoid.LocalizationMap` `instFunLike`	—	`lift_eq` `map_units`
`map_id` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `map` `MonoidHom.id`	—	`lift_id`
`map_injective_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike`	`map` `Submonoid.map` `MonoidHom.instMonoidHomClass` `Submonoid.apply_coe_mem_map`	—	`MonoidHom.instMonoidHomClass` `map_injective_of_surjOn_or_injective` `Submonoid.apply_coe_mem_map` `Set.surjOn_image`
`map_injective_of_surjOn_or_injective` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `Set.SurjOn` `SetLike.coe` `Submonoid.LocalizationMap` `instFunLike`	`map`	—	`map_eq` `surj₂` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `exists_of_eq` `map_units` `eq_iff_exists` `IsUnit.mul_right_cancel`
`map_map` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`map` `MonoidHom.comp`	—	`map_comp_map`
`map_mk'` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`map` `mk'`	—	`map.eq_1` `Submonoid.instSubmonoidClass` `lift_mk'` `mul_inv_left` `mul_mk'_eq_mk'_of_mul` `mk'_mul_cancel_left`
`map_mul_left` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulOne.toMul` `Submonoid.LocalizationMap` `instFunLike` `sec` `map`	—	`mul_comm` `map_mul_right`
`map_mul_right` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`MulOne.toMul` `map` `Submonoid.LocalizationMap` `instFunLike` `sec`	—	`lift_mul_right` `map_units`
`map_spec` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike`	`map` `Submonoid.LocalizationMap` `instFunLike` `sec` `MulOne.toMul`	—	`lift_spec` `map_units`
`map_surjective_of_surjOn` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `Set.SurjOn` `SetLike.coe`	`map`	—	`mk'_surjective` `map_mk'`
`map_surjective_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike`	`map` `Submonoid.map` `MonoidHom.instMonoidHomClass` `Submonoid.apply_coe_mem_map`	—	`MonoidHom.instMonoidHomClass` `map_surjective_of_surjOn` `Submonoid.apply_coe_mem_map` `Set.surjOn_image`
`mulEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfLocalizations` `MonoidHom` `MonoidHom.instFunLike` `lift` `toMonoidHom` `map_units`	—	—
`mulEquivOfLocalizations_left_inv` 📖	mathematical	—	`mulEquivOfLocalizations` `ofMulEquivOfLocalizations`	—	`DFunLike.ext` `isUnit_comp` `DFunLike.ext_iff` `lift_of_comp`
`mulEquivOfLocalizations_left_inv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfLocalizations` `ofMulEquivOfLocalizations`	—	`mulEquivOfLocalizations_left_inv`
`mulEquivOfLocalizations_right_inv` 📖	mathematical	—	`ofMulEquivOfLocalizations` `mulEquivOfLocalizations`	—	`toMonoidHom_injective` `lift_comp` `map_units`
`mulEquivOfLocalizations_right_inv_apply` 📖	mathematical	—	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations` `mulEquivOfLocalizations`	—	`lift_eq` `map_units`
`mulEquivOfLocalizations_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `mulEquivOfLocalizations` `MonoidHom` `MonoidHom.instFunLike` `lift` `toMonoidHom` `map_units`	—	—
`mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations` 📖	mathematical	—	`MulEquiv.symm` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `mulEquivOfLocalizations`	—	—
`mulEquivOfMulEquiv_eq` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfMulEquiv` `Submonoid.LocalizationMap` `instFunLike`	—	`MonoidHom.instMonoidHomClass` `map_eq` `Set.mem_image_of_mem`
`mulEquivOfMulEquiv_eq_map` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`mulEquivOfMulEquiv` `map`	—	`MonoidHom.instMonoidHomClass`
`mulEquivOfMulEquiv_eq_map_apply` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfMulEquiv` `map`	—	`MonoidHom.instMonoidHomClass`
`mulEquivOfMulEquiv_mk'` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `mulEquivOfMulEquiv` `mk'` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Set.mem_image_of_mem` `SetLike.coe`	—	`MonoidHom.instMonoidHomClass` `map_mk'` `Set.mem_image_of_mem`
`ofMulEquivOfDom_apply` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfDom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	`MonoidHom.instMonoidHomClass`
`ofMulEquivOfDom_comp` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom` `MulEquiv.symm` `MulOne.toMul`	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfDom` `MulEquiv` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	`MonoidHom.instMonoidHomClass` `MulEquiv.symm_apply_apply`
`ofMulEquivOfDom_comp_symm` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfDom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm`	—	`MonoidHom.instMonoidHomClass` `MulEquiv.apply_symm_apply`
`ofMulEquivOfDom_eq` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`toMonoidHom` `ofMulEquivOfDom` `MonoidHom.comp`	—	`MonoidHom.instMonoidHomClass`
`ofMulEquivOfDom_id` 📖	mathematical	—	`ofMulEquivOfDom` `MulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`ext` `MonoidHom.instMonoidHomClass` `Submonoid.ext`
`ofMulEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	—
`ofMulEquivOfLocalizations_comp` 📖	mathematical	—	`toMonoidHom` `ofMulEquivOfLocalizations` `MulEquiv.trans` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.comp` `MulEquiv.toMonoidHom`	—	`MonoidHom.ext`
`ofMulEquivOfLocalizations_eq` 📖	mathematical	—	`toMonoidHom` `ofMulEquivOfLocalizations` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulEquiv.toMonoidHom`	—	—
`ofMulEquivOfLocalizations_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm`	—	`Equiv.eq_symm_apply`
`ofMulEquivOfLocalizations_id` 📖	mathematical	—	`ofMulEquivOfLocalizations` `MulEquiv.refl` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`ext`
`of_mulEquivOfMulEquiv` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`toMonoidHom` `ofMulEquivOfLocalizations` `mulEquivOfMulEquiv` `MonoidHom.comp`	—	`MonoidHom.instMonoidHomClass` `MonoidHom.ext` `of_mulEquivOfMulEquiv_apply`
`of_mulEquivOfMulEquiv_apply` 📖	mathematical	`Submonoid.map` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `MonoidHom.instMonoidHomClass` `MulEquiv.toMonoidHom`	`DFunLike.coe` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations` `mulEquivOfMulEquiv` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike`	—	`MonoidHom.instMonoidHomClass` `ext_iff` `mulEquivOfLocalizations_right_inv`
`symm_comp_ofMulEquivOfLocalizations_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations`	—	`MulEquiv.symm_apply_apply`
`symm_comp_ofMulEquivOfLocalizations_apply'` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `Submonoid.LocalizationMap` `instFunLike` `ofMulEquivOfLocalizations` `MulEquiv.symm`	—	`MulEquiv.apply_symm_apply`

---

← Back to Index