Commit 2024-10-21 13:21 3bf558f9

feat(Module/ZLattice): define the pullback of a ZLattice (#16822) Define the pullback of a ZLattice L by a linear map f. The following results are also included:

• If f is a continuous linear equiv, then the pullback is also a ZLattice (added as an instance).
• If f is a linear equiv, define the corresponding basis of the pullback obtained from a basis of L
• If f is a continuous linear equiv and volume preserving, prove that L and its pullback have the same volume. This PR is part of the proof of the Analytic Class Number Formula.