Commit 2024-09-28 16:22 67904bc4

View on Github →

chore: Make Finset.univ_nonempty be simp (#17216) Set.univ_nonempty already is From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/BigOperators/Expect.lean

modified theorem Fintype.expect_one

Modified Mathlib/Data/Fintype/Basic.lean