Theorems · Definition · group theory

AddUnits.opEquiv

{M : Type u_2} → [inst : AddMonoid M] → AddUnits Mᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ

The additive units of the additive opposites are equivalent to the additive opposites of the additive units.

Defined in

Mathlib.Algebra.Group.Units.Opposite

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddMonoid