Mathlib Map

Theorems · Definition · logic and foundations

Equiv.prodComm

(α : Type u_9) → (β : Type u_10) → α × β ≃ β × α

Type product is commutative up to an equivalence: α × β ≃ β × α. This is Prod.swap as an equivalence.

Defined in
Mathlib.Logic.Equiv.Prod
Cited by
55 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.Measure.prod_swap · cited by 14Measure.prod_swapModule.Basis.smulTower · cited by 13Basis.smulTowerYoungDiagram.transpose · cited by 13YoungDiagram.transposeEquiv.punitProd · cited by 9Equiv.punitProdMeasurableEquiv.prodComm · cited by 8MeasurableEquiv.prodCommAlgebra.FormallyUnramified.finite_of_free · cited by 7FormallyUnramified.finite…Module.Basis.smulTower' · cited by 6Basis.smulTower'AddEquiv.prodComm · cited by 5AddEquiv.prodCommEquiv.prodSumDistrib · cited by 5Equiv.prodSumDistribMulEquiv.prodComm · cited by 5MulEquiv.prodCommOrderIso.prodComm · cited by 4OrderIso.prodCommHomeomorph.prodComm · cited by 4Homeomorph.prodCommNat.map_swap_divisorsAntidiagonal · cited by 4Nat.map_swap_divisorsAnti…Module.Basis.smulTower_repr · cited by 4Basis.smulTower_reprAffineEquiv.prodComm · cited by 4AffineEquiv.prodCommEquiv · cited by 8337EquivEquiv.prodCommCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Equivstatement · cited by 8,337

Cited by75

Results whose statement or proof uses this declaration.