Category theory: prod distributes over coprod

Stream: Is there code for X?

[Mario Carneiro]

Is there a proof of A ⨯ (B ⨿ C) ≅ (A ⨯ B) ⨿ (A ⨯ C) somewhere? Is it even true in general?

[Christian Merten]

This is wrong in e.g. vector spaces over a field, since here finite coprod = finite prod.

[Mario Carneiro]

I have a proof using that the category is cartesian closed but it seems like overkill

[Markus Himmel]

Have you seen https://ncatlab.org/nlab/show/distributive+category ? I don't think mathlib has a typeclass for distributive categories.