Commit 2023-02-16 06:27 90742252

View on Github →

Fix: rename Set.to_finset_set_of to Set.toFinset_setOf (#2309)

Estimated changes

Modified Mathlib/Combinatorics/Composition.lean

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Set.toFinset_setOf

deleted theorem Set.to_finset_set_of

Modified Mathlib/Data/Set/Finite.lean