Theorems · Definition · group theory

AddUnits.embedProduct

(α : Type u_6) → [inst : AddMonoid α] → AddUnits α →+ α × αᵃᵒᵖ

Canonical homomorphism of additive monoids from AddUnits α into α × αᵃᵒᵖ. Used mainly to define the natural topology of AddUnits α.

Defined in

Mathlib.Algebra.Group.Prod

Cited by

9 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

AddMonoid