Theorems · Definition · group theory

FreeAbelianGroup.liftAddGroupHom

{α : Type u_2} → (β : Type u_3) → [inst : AddCommGroup β] → FreeAbelianGroup α → (α → β) →+ β

If g : FreeAbelianGroup X and A is an abelian group then liftAddGroupHom g is the additive group homomorphism sending a function X → A to the term of type A corresponding to the evaluation of the induced map FreeAbelianGroup X → A at g.

Defined in

Mathlib.GroupTheory.FreeAbelianGroup

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroup