Commit 2024-08-08 20:12 419ac86b

View on Github →

perf(Data.Nat.Cast.Basic): de-simp theorem with weak keys (#15626) The keys are DFunLike.coe _ _ _ _ _ _ which means we are trying to synthesize two NonAssocSemiring's each time any expression has this as a subterm.

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib/Algebra/Star/CHSH.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

modified theorem WeierstrassCurve.Jacobian.map_addX

modified theorem WeierstrassCurve.Jacobian.map_dblX

Modified Mathlib/Analysis/InnerProductSpace/OfNorm.lean

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean