Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 11:37 271c3237

View on Github →

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

Estimated changes