From 9a23e9df42887ecf9a3f1587ad58dee2db2c518b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 19 Mar 2026 10:31:39 +0100 Subject: [PATCH] perf: lower priority of NormedAlgebraicFoo -> AlgebraicFoo instances We never unbundled the normed and algebra hierarchies, and this is causing performance problems in #36299 and friends. Try if lowering the respective instance priorities helps. --- Mathlib/Analysis/Normed/Group/Defs.lean | 3 +++ Mathlib/Analysis/Normed/Module/Basic.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/Mathlib/Analysis/Normed/Group/Defs.lean b/Mathlib/Analysis/Normed/Group/Defs.lean index 74fd00a79dc773..99dc0878f48750 100644 --- a/Mathlib/Analysis/Normed/Group/Defs.lean +++ b/Mathlib/Analysis/Normed/Group/Defs.lean @@ -196,6 +196,9 @@ class NormedGroup (E : Type*) extends Norm E, Group E, MetricSpace E where /-- The distance function is induced by the norm. -/ dist_eq : ∀ x y, dist x y = ‖x⁻¹ * y‖ := by aesop +/- TODO: comment on this change! -/ +attribute [instance 900] NormedAddGroup.toAddGroup SeminormedAddGroup.toAddGroup + /-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines a pseudometric space structure. -/ class SeminormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E, diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean index d369e5ef2e1346..c8b221609315d6 100644 --- a/Mathlib/Analysis/Normed/Module/Basic.lean +++ b/Mathlib/Analysis/Normed/Module/Basic.lean @@ -271,6 +271,9 @@ class NormedAlgebra (𝕜 : Type*) (𝕜' : Type*) [NormedField 𝕜] [Seminorme Algebra 𝕜 𝕜' where norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ‖r • x‖ ≤ ‖r‖ * ‖x‖ +/- TODO comment on this change! -/ +attribute [instance 900] NormedAlgebra.toAlgebra + attribute [inherit_doc NormedAlgebra] NormedAlgebra.norm_smul_le variable (𝕜')