Commit 2025-08-29 09:05 d4131b7d

View on Github →

refactor(NumberTheory/LSeries): move evaluation argument s to last in LSeries_congr (#29060) Align with Mathlib convention of having evaluation variables last, improving readability, partial application, and consistency with derivative/continuity lemmas. Previously, s was first, which was slightly off-pattern and less ergonomic in pipelines.

Estimated changes