Structures · Algebra
AddMonoidHomClass
AddMonoidHomClass F M N states that F is a type of AddZero-preserving
homomorphisms.
You should also extend this typeclass when you extend AddMonoidHom.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Shape
- 3 explicit arguments
Extends2
Extended by4
Concrete types that are instances11
- AddMonoid.End
- AddMonoidHom
- NormedAddGroupHom
- ContinuousAddMonoidHom
- Derivation
- AddHom
- OrderAddMonoidHom
- ContMDiffAddMonoidMorphism
- AddSubmonoid.LocalizationMap
- AddGroupExtension.Splitting
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by286
- map_sub
- map_sum
- map_neg
- AddMonoidHomClass.toAddMonoidHom
- AddSubmonoid.map
- injective_iff_map_eq_zero
- AddSubmonoid.comap
- AddMonoidHom.mrange
- map_finsuppSum
- map_nsmul
- HasSum.map
- map_list_sum
- map_multiset_sum
- AddMonoidHom.mker
- AddMonoidHomClass.isometry_of_norm
- map_zsmul
- IsAddUnit.map
- AddSubmonoid.gc_map_comap
- AddMonoidHom.mrange_eq_map
- ContinuousAddMonoidHom.toContinuousAddMonoidHom
- AddMonoidHom.map_mclosure
- uniformContinuous_of_continuousAt_zero
- injective_iff_map_eq_zero'
- AddMonoidHom.mem_mrange
- IsSemilinearSet.image
- AddSubmonoid.giMapComap
- AddMonoidHom.mrange_eq_top
- Function.LeftInverse.map_tsum
- AddSubmonoid.gciMapComap
- map_inv_natCast_smul
- AddSubmonoid.mem_comap
- AddMonoidHomClass.antilipschitz_of_bound
- map_dfinsuppSum
- AddMonoidHom.coe_coe
- uniformContinuous_addMonoidHom_of_continuous
- AddMonoidHom.mrange_eq_top_of_surjective
- topologicalAddGroup_induced
- AddMonoidHomClass.lipschitz_of_bound
- Topology.IsClosedEmbedding.map_tsum
- Multiset.sum_hom
- continuous_of_continuousAt_zero
- map_add_eq_zero
- map_rat_smul
- OrderMonoidHomClass.toOrderAddMonoidHom
- Summable.map
- AddMonoidHom.coe_mrange
- Summable.map_iff_of_leftInverse
- Summable.map_tsum
- isAddCyclic_of_surjective
- AddMonoidHomClass.isometry_iff_norm