Structures · Algebra
AddEquivClass
AddEquivClass F A B states that F is a type of addition-preserving morphisms.
You should extend this class when you extend AddEquiv.
- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Shape
- 3 explicit arguments · adds map_add
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- AddEquiv
- OrderAddMonoidIso
- ContinuousAddEquiv
- AddGroupExtension.Equiv
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- AddEquivClass.toAddEquiv
- AddEquivClass.coe_symm_apply_apply
- map_finsetSum
- isSemilinearSet_image_iff
- Summable.map_iff_of_equiv
- Submodule.natAbs_det_equiv
- AddEquivClass.apply_mem_center
- AddSubgroup.map_equiv_top
- AddEquivClass.map_finsum
- AddEquivClass.map_add
- AddEquiv.isAddUnit_map
- Ideal.natAbs_det_equiv
- AddEquiv.addIrreducible_iff
- AddEquivClass.apply_coe_symm_apply
- AddEquiv.toRingEquiv
- instCoeTCOrderAddMonoidIsoOfOrderIsoClassOfAddEquivClass
- AddEquivClass.isDedekindFiniteAddMonoid_iff
- AddSubmonoid.map_coe_toAddEquiv
- AddEquivClass.apply_mem_center_iff
- instCoeTCAddEquivOfAddEquivClass
- AddEquivClass.toAddEquiv.congr_simp
- AddEquivClass.instAddHomClass
- AddIrreducible.map
- AddEquivClass.toAddEquiv_injective
- OrderMonoidIsoClass.toOrderAddMonoidIso
- AddEquivClass.instAddMonoidHomClass
- AddEquivClass.isAddFreimanIso
- map_finset_sum
- AddSubmonoid.IsLocalizationMap.addEquiv_comp
Ancestors0
No ancestors.