feat(LinearAlgebra/Dimension): tower law for algebraic extensions

[ChiCubed]

We generalise the tower law for Module.rank to the situation of a module over an algebraic extension of domains.

---

See the Zulip thread for some associated discussion.

I am not sure about in which file these results should live, or what their names should be. For the file I have gone with LinearAlgebra/Dimension/Algebraic.lean for now, because these feel more like dimension theorems than Algebra.IsAlgebraic theorems, and IMO do not logically fit into the other existing files in LinearAlgebra/Dimension.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary c323074686

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Dimension.Domain (new file)	1806

---

Declarations diff (regex)

+ IsTorsionFree.erank_mul_erank
+ IsTorsionFree.finrank_mul_finrank
+ finrank_mul_finrank
+ finrank_mul_finrank_of_field_isLocalization
+ finrank_mul_finrank_of_isFractionRing_isLocalization
+ lift_rank_mul_lift_rank
+ lift_rank_mul_lift_rank_of_field_isLocalization
+ lift_rank_mul_lift_rank_of_isFractionRing_isLocalization
+ of_semifield_isLocalization
+ rank_mul_rank
+ rank_mul_rank_of_field_isLocalization
+ rank_mul_rank_of_isFractionRing_isLocalization

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 -- stale, waiting for the new build)

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

• +12 new declarations
• −0 removed declarations

+Algebra.IsAlgebraic.finrank_mul_finrank
+Algebra.IsAlgebraic.lift_rank_mul_lift_rank
+Algebra.IsAlgebraic.rank_mul_rank
+IsFractionRing.of_semifield_isLocalization
+Module.IsTorsionFree.erank_mul_erank
+Module.IsTorsionFree.finrank_mul_finrank
+Module.finrank_mul_finrank_of_field_isLocalization
+Module.finrank_mul_finrank_of_isFractionRing_isLocalization
+Module.lift_rank_mul_lift_rank_of_field_isLocalization
+Module.lift_rank_mul_lift_rank_of_isFractionRing_isLocalization
+Module.rank_mul_rank_of_field_isLocalization
+Module.rank_mul_rank_of_isFractionRing_isLocalization

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit c323074686
Reference commit dec5b2b780

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

[mathlib-merge-conflicts]

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

[ChiCubed]

I noticed some improvements are possible to #41614 when merging but it'll be a nontrivial amount of code so I'll make it a different PR

[themathqueen]

I noticed some improvements are possible to #41614 when merging but it'll be a nontrivial amount of code so I'll make it a different PR

I think it would be better if you merge master and just do it now.

[ChiCubed]

OK. Let me know if you want me to split it up after all, the diff ended up a bit bigger than I was expecting.
My new definition of Module.finrank_mul_finrank' is technically not strictly more general, but the (bad) difference comes from what was a golfed-away IsDomain S assumption that just follows immediately from FaithfulSMul S T. So it should be better for all practical purposes.

[ChiCubed]

-awaiting-author

[tb65536]

No need for some of these newlines.

Suggested change

	theorem finrank_mul_finrank :
	finrank R S * finrank S M = finrank R M :=
	theorem finrank_mul_finrank : finrank R S * finrank S M = finrank R M :=

[ChiCubed]

I edited the two near that but left others unchanged despite being able to fit on one line within col limit (since I find that for long theorem names it makes it hard to tell what the type is at a glance)

[ChiCubed]

-awaiting-author