[Merged by Bors] - feat(Module/ZLattice): define the pullback of a ZLattice

[xroblot]

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.

---

[github-actions]

PR summary 96173177b4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Basis.ofZLatticeComap
+ Basis.ofZLatticeComap_apply
+ Basis.ofZLatticeComap_repr_apply
+ ZLattice.coe_comap
+ ZLattice.comap
+ ZLattice.comap_comp
+ ZLattice.comap_discreteTopology
+ ZLattice.comap_equiv
+ ZLattice.comap_equiv_apply
+ ZLattice.comap_refl
+ ZLattice.comap_span_top
+ covolume_comap
+ instIsZLatticeComap
+ instance [DiscreteTopology L] (e : F ≃L[K] E) :
+ map

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[jcommelin]

bors d+

[mathlib-bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build