Theorems · Inductive type · group theory

AddHom

(M : Type u_10) → (N : Type u_11) → [Add M] → [Add N] → Type (max u_10 u_11)

M →ₙ+ N is the type of functions M → N that preserve addition. The ₙ in the notation stands for "non-unital" because it is intended to match the notation for NonUnitalAlgHom and NonUnitalRingHom, so a AddHom is a non-unital additive monoid hom. When possible, instead of parametrizing results over (f : AddHom M N), you should parametrize over (F : Type*) [AddHomClass F M N] (f : F). When you extend this structure, make sure to extend AddHomClass.

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

294 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

AddAdd