feat(GCDMonoid): Associates form DistribLattice

[alreadydone]

Co-authored-by: Aaron Liu @plp127

Import increase to two modified files are 2~3%, maybe I'll create another file GCDMonoid.Lattice for the new results.

---

• depends on: feat(Order): constructors for DistribLattice and IsModularLattice #41666

[github-actions]

PR summary bbf55a2eff

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.Lattice.Constructor (new file)	189
Mathlib.Algebra.GCDMonoid.Lattice (new file)	433

---

Declarations diff (regex)

+ Associates.distribLattice
+ DistribLattice.ofSupInfLeAssoc
+ associated_gcd_lcm_left
+ associated_gcd_lcm_right
+ associated_lcm_gcd_left
+ associated_lcm_gcd_right
+ isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup
+ ofEqOfInfSupEq
+ ofInfSupLeSupInf
++ gcd_lcm_left
++ gcd_lcm_right
++ lcm_gcd_left
++ lcm_gcd_right

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit bbf55a2).

• +17 new declarations
• −0 removed declarations

+Associates.distribLattice
+DistribLattice.ofEqOfInfSupEq
+DistribLattice.ofInfSupLeSupInf
+DistribLattice.ofSupInfLeAssoc
+Nat.gcd_lcm_left
+Nat.gcd_lcm_right
+Nat.lcm_gcd_left
+Nat.lcm_gcd_right
+associated_gcd_lcm_left
+associated_gcd_lcm_right
+associated_lcm_gcd_left
+associated_lcm_gcd_right
+gcd_lcm_left
+gcd_lcm_right
+isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup
+lcm_gcd_left
+lcm_gcd_right

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit bbf55a2eff
Reference commit 4efb186f10

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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!

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Order): constructors for DistribLattice and IsModularLattice #41666
  By Dependent Issues (🤖). Happy coding!