Commit 2026-05-13 06:56 defda893

View on Github →

chore(*): reduce defeq abuse of Set α = α → Prop (#39019)

Estimated changes

Modified Mathlib/Analysis/Complex/CoveringMap.lean

Modified Mathlib/Analysis/Normed/Group/FunctionSeries.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/NumberTheory/EulerProduct/ExpLog.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

modified theorem Multipliable.subtype

Modified Mathlib/Topology/FiberBundle/Basic.lean