Def Set.subtypeInsertEquivOption

Modification history

2025-02-09 06:38

Mathlib/Data/Set/Basic.lean

chore(Data/Set/Basic): split `insert` / `singleton` / `pair` to new file (#21567) …

Modified Set.subtypeInsertEquivOption View on Github →

2024-10-30 05:09

Mathlib/Data/Set/Basic.lean

feat(RingTheory/AlgebraicIndependent): add some results on `AlgebraicIndependent` (#18378) …

Added Set.subtypeInsertEquivOption View on Github →