feat(Algebra/Module/ZLattice): align ZSpan.floor to Int.floor API

[ster-oc]

This PR adds some of the existent lemmas about Int.floor, Int.ceil and Int.fract to the ZSpan namespace.

---

[github-actions]

PR summary f7ee1844c2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ceil_add_coe
+ ceil_coe_add
+ ceil_eq_iff
+ ceil_eq_on_vadd_fundamentalDomain
+ ceil_eq_self_iff_mem
+ ceil_eq_zero_iff
+ ceil_sub_coe
+ ceil_zero
+ floor_add_fract
+ floor_add_zSpanCast
+ floor_coe_add
+ floor_eq_iff
+ floor_eq_on_vadd_fundamentalDomain
+ floor_eq_self_iff_mem
+ floor_eq_zero_iff
+ floor_fract
+ floor_sub_coe
+ floor_zero
+ fract_add
+ fract_add_coe
+ fract_add_floor
+ fract_coe_add
+ fract_eq_iff
+ fract_eq_zero_iff
+ fract_ext
+ fract_floor
+ fract_ne_zero_iff
+ fract_neg_eq_zero
+ fract_sub_self
+ fract_zSpanCast
+ fract_zero
+ mem_neg_fundamentalDomain
+ mem_vadd_fundamentalDomain
+ mem_vadd_neg_fundamentalDomain
+ preimage_ceil_singleton
+ preimage_floor_singleton
+ self_sub_floor
+ self_sub_fract
- Zlattice.FG
- ceil_eq_self_of_mem
- floor_eq_self_of_mem
- fract_add_ZSpan
- fract_apply
- fract_zSpan_add

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 scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[ster-oc]

@joelriou thanks for the review!

I called them floor_mem_add and floor_add_mem to highlight on which side the member of the lattice is, otherwise the name would have been the same.

This branch grew a bit locally. I ended up adding some other lemmas, relaxed the hypotheses to [Ring K] here and there, and some other minor fixes. Should I push the branch here and change the name of the PR or is it not useful?

-awaiting-author

[joelriou]

@joelriou thanks for the review!

I called them floor_mem_add and floor_add_mem to highlight on which side the member of the lattice is, otherwise the name would have been the same.

This branch grew a bit locally. I ended up adding some other lemmas, relaxed the hypotheses to [Ring K] here and there, and some other minor fixes. Should I push the branch here and change the name of the PR or is it not useful?

-awaiting-author

Ok, then, my understanding is that floor_coe_add_of_mem and floor_add_coe_of_mem would be better names.
As the PR is short, do not hesitate to update it or add more material.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[ster-oc]

Sparse thoughts:

• Instead of (m : M) (hm : m ∈ span ℤ (Set.range b)) I think it would be good to use (m : span ℤ (Set.range b)) which is what most of the time people would deal with (and it is already used here and there in the API).
• I am thinking about moving vadd_mem_fundamentalDomain in section floor and call it neg_floor_eq_iff or something like that.
• I am still golfing the proofs a bit.
• Probably with a bit of work one could define an attribute [to_zspan] to get rid of the newborn sections almost completely.
• I was alto thinking to abbrev span ℤ (Set.range b)) to ZSpan b but again this is a style choice out of my competence

-awaiting-author