CategoryTheory.Limits.HasBinaryProduct.swap

theorem CategoryTheory.Limits.HasBinaryProduct.swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q], CategoryTheory.Limits.HasBinaryProduct Q P

The theorem `CategoryTheory.Limits.HasBinaryProduct.swap` states that, for any category `C`, and any two objects `P` and `Q` in `C`, if there is a binary product of `P` and `Q`, then there is also a binary product of `Q` and `P`. Essentially, the order of the two objects in the definition of the binary product doesn't matter. This theorem cannot be declared as an instance as it would cause a loop in the typeclass search.

More concisely: If object `P` and `Q` in category `C` have a binary product, then so do `Q` and `P`.