Theorems · Definition · group theory

Units.mapEquiv

{M : Type u_3} → {N : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid N] → M ≃* N → Mˣ ≃* Nˣ

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Defined in

Mathlib.Algebra.Group.Units.Equiv

Cited by

16 results in Mathlib

Foundations

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

Assumes

MonoidMonoid