mathlib
271c3237 - feat(order/filter): prod_assoc (#12002)

Commit

3 years ago

feat(order/filter): prod_assoc (#12002) map (prod_assoc α β γ) ((f ×ᶠ g) ×ᶠ h) = f ×ᶠ (g ×ᶠ h) with two tiny supporting lemmas

Author

PatrickMassot

Parents