Skip to content

Commit

Permalink
perf: reduce instance priority of Complex.instSMulRealComplex (#12070)
Browse files Browse the repository at this point in the history
See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20prefers.20CharP.2Ecast_eq_zero.20over.20Nat.2Ecast_zero/near/432760180) on Zulip.

We reduce the instance priority of `Complex.instSMulRealComplex` to 90. This leads to a very significant speed-up in two Modular Forms files (and still noticeable speed-ups in some other files).
  • Loading branch information
MichaelStollBayreuth committed Apr 12, 2024
1 parent 5dd5b45 commit a743f61
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion Mathlib/Data/Complex/Basic.lean
Expand Up @@ -352,7 +352,10 @@ variable {R : Type*} [SMul R ℝ]

/- The useless `0` multiplication in `smul` is to make sure that
`RestrictScalars.module ℝ ℂ ℂ = Complex.module` definitionally. -/
instance instSMulRealComplex : SMul R ℂ where
-- priority manually adjusted in #12070, to avoid situations like instance synthesis
-- of `SMul ℂ ℂ` trying to proceed via `SMul ℂ ℝ`.
-- See issue #11692.
instance (priority := 90) instSMulRealComplex : SMul R ℂ where
smul r x := ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩

theorem smul_re (r : R) (z : ℂ) : (r • z).re = r • z.re := by simp [(· • ·), SMul.smul]
Expand Down

0 comments on commit a743f61

Please sign in to comment.