feat(Algebra): depth of QuotSMulTop

[Thmoas-Guan]

In this PR, we proved for a local ring R and a finitely generated R module M N, IsSMulRegular M x and x ∈ Module.annihilator R N, then depth(N, M/xM) + 1 = depth(N, M), and its corollary for quotient regular seqence.

---

• [ ] depends on: #26214

[Thmoas-Guan]

This PR is originally from #25109

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#26214 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 86622378a5

Import changes exceeding 2%

%	File
+42.10%	Mathlib.RingTheory.Regular.Category
+26.90%	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	1991	+422 (+26.90%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Regular.Depth	422
Mathlib.RingTheory.Regular.Category	509

---

Declarations diff

+ Ideal.depth + Ideal.depth_eq_of_iso + Ideal.depth_quotSMulTop_succ_eq_moduleDepth + Ideal.quotient_smul_top_lt_of_le_smul_top + IsLocalRing.depth + IsLocalRing.depth_eq_of_algebraMap_surjective + IsLocalRing.depth_eq_of_iso + IsLocalRing.depth_eq_of_ringEquiv + IsLocalRing.depth_eq_sSup_length_regular + IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth + IsLocalRing.depth_quotient_regular_sequence_add_length_eq_depth + IsLocalRing.depth_quotient_regular_succ_eq_depth + IsLocalRing.depth_quotient_span_regular_succ_eq_depth + IsLocalRing.ideal_depth_eq_sSup_length_regular + IsLocalRing.ideal_depth_le_depth + Submodule.comap_lt_top_of_lt_range + Submodule.smul_top_eq_comap_smul_top_of_surjective + depth_quotient_regular_sequence_add_length_eq_depth + exists_isRegular_of_exists_subsingleton_ext + exists_isRegular_tfae + ext_subsingleton_of_exists_isRegular + ext_subsingleton_of_lt_moduleDepth + ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth + moduleDepth + moduleDepth_eq_depth_of_supp_eq + moduleDepth_eq_find + moduleDepth_eq_iff + moduleDepth_eq_moduleDepth_shrink + moduleDepth_eq_of_iso_fst + moduleDepth_eq_of_iso_snd + moduleDepth_eq_sSup_length_regular + moduleDepth_eq_sup_nat + moduleDepth_eq_top_iff + moduleDepth_eq_zero_of_hom_nontrivial + moduleDepth_ge_min_of_shortExact_fst_fst + moduleDepth_ge_min_of_shortExact_fst_snd + moduleDepth_ge_min_of_shortExact_snd_fst + moduleDepth_ge_min_of_shortExact_snd_snd + moduleDepth_ge_min_of_shortExact_trd_fst + moduleDepth_ge_min_of_shortExact_trd_snd + moduleDepth_lt_top_iff + moduleDepth_quotSMulTop_succ_eq_moduleDepth + moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth + mono_postcomp_mk₀_of_mono + mono_precomp_mk₀_of_epi + postcomp_mk₀_injective_of_mono + pow_mono_of_mono + precomp_mk₀_injective_of_epi + ring_depth_invariant + ring_depth_uLift + 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).

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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