Theorem Equiv.Finset.congr_refl

Modification history

2026-08-31 14:42

Mathlib/Data/Finset/Image.lean

chore: rename `Equiv.Set.congr` to `Set.equivOfEq` (#43200) …

Deleted Equiv.Finset.congr_refl View on Github →

2026-08-28 20:31

Mathlib/Data/Finset/Image.lean

chore(Logic/Equiv): swap the names of `Equiv.setCongr` and `Equiv.Set.congr` (#43005) …

Modified Equiv.Finset.congr_refl View on Github →

2026-08-11 15:45

Mathlib/Data/Finset/Image.lean

chore: improve `Set` / `Finset` congruence API (#42640) …

Added Equiv.Finset.congr_refl View on Github →