Theorems · Definition · group theory

MonoidHom.toHomUnits

{G : Type u_1} → {M : Type u_2} → [inst : Group G] → [inst_1 : Monoid M] → (G →* M) → G →* Mˣ

If f is a homomorphism from a group G to a monoid M, then its image lies in the units of M, and f.toHomUnits is the corresponding monoid homomorphism from G to Mˣ.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

9 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

GroupMonoid