Commit 2024-09-13 07:28 c3c78bbd
View on Github →chore: refactor ZLattice to Submodule ℤ (#16604)
For some reason, ZLattice is an AddSubgroup, but it appears that life would be simpler if it were a Submodule ℤ. it is also consistent with the ZSpan construction of ℤ-lattices. This is what this PR does. See also this Zulip thread.
This PR is part of the proof of the Analytic Class Number Formula.