Theorems · Definition · group theory

AddEquiv.prodAddUnits

{M : Type u_3} →
  {N : Type u_4} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddUnits (M × N) ≃+ AddUnits M × AddUnits N

The additive monoid equivalence between additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Defined in

Mathlib.Algebra.Group.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoid