Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-15 09:58
2e99d8af
View on Github →
chore(Data/Finset): drop 2
DecidableEq
assumptions (
#10575
) In 1 case, golf the proof.
Estimated changes
Modified
Mathlib/Data/Finset/Basic.lean
modified
theorem
Finset.Nonempty.exists_cons_eq
modified
theorem
Finset.Nontrivial.exists_cons_eq