Commit 2023-12-25 13:26 ef974f86

View on Github →

chore(*): use ∃ x ∈ s, _ instead of ∃ (x) (_ : x ∈ s), _ (#9215) Follow-up #9184

Estimated changes

modified theorem Interval.bot_pow
modified theorem DFinsupp.support_subset_iff
modified theorem Fintype.prod_eq_single
modified theorem nodup_permsOfList
modified theorem Int.ediv_dvd_ediv
modified def Nat.evenOddRec
modified theorem Part.ext'