Commit 2026-08-28 20:31 05322f90

View on Github →

chore(Logic/Equiv): swap the names of Equiv.setCongr and Equiv.Set.congr (#43005) The new Equiv.setCongr matches MulEquiv.monoidHomCongrLeft and friends. Perform the same change for Finset. Follow-up to #42640. Generated by Claude Sonnet, reviewed and improved line-by-line by myself. Assisted-by: Claude Sonnet 5

Estimated changes

deleted theorem Equiv.Finset.congr_apply
modified theorem Equiv.Finset.congr_refl
modified theorem Equiv.Finset.congr_symm
modified theorem Equiv.Finset.congr_trans
modified def Equiv.finsetCongr
modified theorem Equiv.finsetCongr_refl
modified theorem Equiv.finsetCongr_symm
modified theorem Equiv.finsetCongr_trans
modified def Equiv.setCongr
deleted def OrderIso.setCongr