Commit 2025-03-20 04:39 7b2dab25

View on Github →

chore: deprecate Equiv.Set.ofEq (#23119) Replace with Equiv.setCongr, defined earlier in the same file.

Estimated changes

Modified Archive/Imo/Imo1987Q1.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Equiv.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Fintype/Sort.lean

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

Modified Mathlib/Order/Partition/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean