Def Equiv.sigmaEquivOptionOfInhabited

Modification history

2025-03-20 03:52

Mathlib/Logic/Equiv/Basic.lean

chore(Logic/Equiv): split some chunks off large file `Equiv/Basic.lean` (#23099) …

Modified Equiv.sigmaEquivOptionOfInhabited View on Github →

2024-02-13 21:51

Mathlib/Data/Finset/Basic.lean

chore: Move `Equiv.sigmaEquivOptionOfInhabited` (#10501) …

Modified Equiv.sigmaEquivOptionOfInhabited View on Github →

2023-01-16 08:13

Mathlib/Data/Finset/Basic.lean

feat: port Data.Finset.Basic (#1555)

Added Equiv.sigmaEquivOptionOfInhabited View on Github →