mathlib3 documentation


Preserving binary products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.

In particular, we show that prod_comparison G X Y is an isomorphism iff G preserves the product of X and Y.