mathlib4 feat(Algebra): the Rees theorem for depth

In this PR we proved the Rees theorem for depth.

Co-authored-by: Hu Yongle [email protected]

[x] depends on: #27416

Jun 20 '25 11:06 Thmoas-Guan

This PR is originally from #24249

Jun 20 '25 12:06 Thmoas-Guan

PR summary 86622378a5

Import changes exceeding 2%

%	File
+42.10%	`Mathlib.RingTheory.Regular.Category`
+26.83%	`Mathlib.RingTheory.Regular.Depth`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Category	1209	1718	+509 (+42.10%)
Mathlib.RingTheory.Regular.Depth	1569	1990	+421 (+26.83%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Regular.Depth`	421
`Mathlib.RingTheory.Regular.Category`	509

Declarations diff

+ Ideal.quotient_smul_top_lt_of_le_smul_top + Submodule.smul_top_eq_comap_smul_top_of_surjective + exists_isRegular_of_exists_subsingleton_ext + exists_isRegular_tfae + ext_subsingleton_of_exists_isRegular + pow_mono_of_mono + smul_id_postcomp_eq_zero_of_mem_ann

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.

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).