Commit 2024-02-12 10:30 e5de077c

View on Github →

chore(SetFamily/FourFunctions): drop some unneeded DecidableEq assumptions (#10442)

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean

modified theorem Finset.le_card_infs_mul_card_sups

modified theorem four_functions_theorem