Commit 2026-08-31 14:42 ffbb7e43

View on Github →

chore: rename Equiv.Set.congr to Set.equivOfEq (#43200) and similarly for Finset and OrderIso. This matches the general Subfoo.fooEquivOfEq pattern already used elsewhere in mathlib. Generated by Claude Opus Assisted-by: Claude Opus 5

Estimated changes

deleted theorem Equiv.Finset.congr_refl
deleted theorem Equiv.Finset.congr_symm
deleted theorem Equiv.Finset.congr_trans
added def Finset.equivOfEq
added theorem Finset.equivOfEq_refl
added theorem Finset.equivOfEq_symm
added theorem Finset.equivOfEq_trans
deleted theorem Equiv.strictMono_setCongr
added def Set.equivOfEq
added def Set.orderIsoOfEq