Theorems · Definition · group theory

AddEquiv.prodComm

{M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M × N ≃+ N × M

The equivalence between M × N and N × M given by swapping the components is additive.

Defined in

Mathlib.Algebra.Group.Prod

Cited by

5 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

AddZeroClassAddZeroClass