Commit 2025-07-31 23:59 553449cc

View on Github →

chore: remove some duplicate instances (#25410) I have a program that finds duplicate instances, as described at #mathlib4 > duplicate declarations This PR is a start at fixing these in Mathlib.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Group/Fin/Basic.lean

Modified Mathlib/Algebra/Homology/Embedding/IsSupported.lean

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

Modified Mathlib/Algebra/Ring/Divisibility/Basic.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/CategoryTheory/Countable.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

Modified Mathlib/CategoryTheory/ObjectProperty/FullSubcategory.lean

Modified Mathlib/Computability/TuringDegree.lean

Modified Mathlib/Data/ENat/Basic.lean

Modified Mathlib/Data/Fintype/EquivFin.lean

Modified Mathlib/Data/List/TakeDrop.lean

Modified Mathlib/Data/Matroid/Constructions.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Option/Defs.lean

added theorem Option.merge_isAssociative

added theorem Option.merge_isCommutative

added theorem Option.merge_isId

added theorem Option.merge_isIdempotent

Modified Mathlib/Data/Ordering/Basic.lean

Modified Mathlib/Data/Sign/Defs.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Logic/Equiv/Fin/Basic.lean

added theorem subsingleton_fin_one

added theorem subsingleton_fin_zero

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean