Commit 2026-03-05 10:25 237efa90

View on Github →

chore(*): reduce defeq abuse about Set (#36152) Also fix some /- <-> /-- typos I've noticed while fixing defeq abuse.

Estimated changes

Modified Mathlib/Analysis/Complex/CoveringMap.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

modified theorem ContinuousLinearMapWOT.hasBasis_seminorms

Modified Mathlib/Combinatorics/Derangements/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

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

Modified Mathlib/Order/CompleteLatticeIntervals.lean

Modified Mathlib/Order/Interval/Set/OrdConnected.lean

Modified Mathlib/Order/Interval/Set/OrderIso.lean

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean

Modified Mathlib/RingTheory/Ideal/IsPrincipal.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Finite.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

modified theorem Cardinal.mk_set

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/Constructions/SumProd.lean

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/IndicatorConstPointwise.lean

Modified Mathlib/Topology/Instances/Complex.lean

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/IsClosedRestrict.lean

Modified Mathlib/Topology/LocalAtTarget.lean

Modified Mathlib/Topology/MetricSpace/CantorScheme.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified Mathlib/Topology/MetricSpace/Thickening.lean

Modified Mathlib/Topology/Metrizable/Urysohn.lean

Modified Mathlib/Topology/Order.lean

modified theorem TopologicalSpace.mkOfClosure_sets

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Order/HullKernel.lean

Modified Mathlib/Topology/Perfect.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean