Commit 2024-02-13 21:51 3b447547

View on Github →

chore: Move Equiv.sigmaEquivOptionOfInhabited (#10501) This has nothing to do with Finset

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

deleted def Equiv.sigmaEquivOptionOfInhabited

Modified Mathlib/Logic/Equiv/Basic.lean

added def Equiv.sigmaEquivOptionOfInhabited