Theorems · Definition · logic and foundations
Equiv.sumComm
(α : Type u_9) → (β : Type u_10) → α ⊕ β ≃ β ⊕ α
Sum of types is commutative up to an equivalence. This is Sum.swap as an equivalence.
- Defined in
- Mathlib.Logic.Equiv.Sum
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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 by35
Results whose statement or proof uses this declaration.
- Equiv.sumComm_applystatement and proof · cited by 17
- MvPolynomial.tensorEquivSumproof · cited by 13
- Polynomial.resultant_commproof · cited by 11
- finAddFlipproof · cited by 5
- SimpleGraph.Iso.sumCommproof · cited by 5
- WithBot.orderIsoPUnitSumLexproof · cited by 4
- Diffeomorph.sumCommproof · cited by 4
- OrderIso.sumLexDualAntidistribproof · cited by 4
- Equiv.emptySumproof · cited by 4
- Equiv.sumSumSumCommproof · cited by 3
- Homeomorph.sumCommproof · cited by 3
- MvPolynomial.tensorEquivSum_X_tmul_oneproof · cited by 3