Commit 2024-02-09 21:00 e7d5230e
View on Github →chore(NumberTheory/LSeries): create directory, move file (#10385)
This PR creates a new directory Mathlib/NumberTheory/LSeries and moves the file Mathlib/NumberTheory/LSeries.lean to Mathlib/NumberTheory/LSeries/Basic.lean.
This is in preparation of adding more material on L-series. See here on Zulip.