feat (Lattice/Covolume): Add results linking point counting in lattices and covolume

[xroblot]

---

• depends on: feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals #12405
• depends on: [Merged by Bors] - feat(Module/ZLattice): define the pullback of a ZLattice #16822

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals #12405
• [Merged by Bors] - feat(Module/ZLattice): define the pullback of a ZLattice #16822
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 80a33e3d7a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.ZLattice.Covolume	1832	1854	+22 (+1.20%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.Units.Regulator	1
Mathlib.Algebra.Module.ZLattice.Covolume	22
Mathlib.Analysis.BoxIntegral.UnitPartition	1848

---

Declarations diff

+ Basis.det_basis
+ Basis.det_inv
+ Basis.ofZLatticeBasis_comap
+ BoxIntegral.hasIntegralCorners
+ BoxIntegral.le_hasIntegralVertices_of_isBounded
+ ContinuousOn.continuousAt_mulIndicator
+ Pi.basisFun_det_apply
+ admissibleIndex
+ box
+ box_index_tag_eq_self
+ box_injective
+ box_lower
+ box_upper
+ covolume_eq_det_inv
+ diam_boxIcc
+ disjoint
+ eqOn_mulIndicator'
+ eq_of_index_eq_index_and_mem_smul_span
+ exists_admissibleIndex
+ index
+ index_apply
+ index_tag
+ integralSum_eq_tsum_div
+ isBounded
+ isBounded_Icc
+ mem_admissibleIndex_iff
+ mem_admissibleIndex_of_mem_box
+ mem_admissibleIndex_of_mem_box_aux₁
+ mem_admissibleIndex_of_mem_box_aux₂
+ mem_box_iff
+ mem_box_iff'
+ mem_box_iff_index
+ mem_prepartition_boxes_iff
+ mem_prepartition_iff
+ prepartition
+ prepartition_isHenstock
+ prepartition_isPartition
+ prepartition_isSubordinate
+ prepartition_tag
+ repr_isUnitSMul
+ setFinite_index
+ setFinite_inter
+ smul
+ tag
+ tag_apply
+ tag_index_eq_self_of_mem_smul_span
+ tag_injective
+ tag_mem
+ tag_mem_smul_span
+ tendsto_card_div_pow''
+ tendsto_card_le_div
+ tendsto_card_le_div'
+ tendsto_card_le_div''
+ tendsto_tsum_div_pow
+ volume_box
+ volume_image_eq_volume_div_covolume
+ volume_image_eq_volume_div_covolume'
++ tendsto_card_div_pow
++ tendsto_card_div_pow'

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.