feat(RingTheory/Finiteness/Basic): add lemmas for restricting scalars

[martinwintermath]

This PR adds three lemmas that transfer Submodule.FG across restricting scalars from a semiring A to a semiring R under the assumption Module.Finite R A . This includes

• fg_restrictScalars which proves that restrictScalars preserves FG
• fg_restrictScalars_iff as the iff version of the above
• span_submodule_fg_of_fg which proves that the A-span of an FG R-submodule is FG.

The PR also contains the following changes to related lemmas:

• renaming fg_restrictScalars to fg_restrictScalars_of_surjective emphasizing the hypothesis Function.Surjective (algebraMap R A)
• adding a sections RestrictScalars that also contains the above lemma
• restructuring variables in the above section

---

[github-actions]

PR summary e760ec41db

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ fg_restrictScalars_iff
+ fg_restrictScalars_of_surjective
+ span_submodule_fg_of_fg

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

[LLaurance]

It looks like you are renaming Submodule.fg_restrictScalars here and defining a new Submodule.fg_restrictScalars at around line 414. To avoid confusion I suggest renaming your other new theorem to Submodule.FG.restrictScalars and adding a deprecation notice for this theorem:

@[deprecated (since := "2026-01-24")] alias fg_restrictScalars := fg_restrictScalars_of_surjective

[LLaurance]

May as well refactor by having variable {S : Submodule A M} and changing N to S in fg_restrictScalars_of_surjective.

[LLaurance]

See https://github.com/leanprover-community/mathlib4/pull/33980/changes#r2723788975

[LLaurance]

Perhaps R could be made implicit?

[LLaurance]

Suggested change

	theorem span_submodule_fg_of_fg {S : Submodule R M} (hfg : S.FG) :
	(span A S : Submodule A M).FG := by
	obtain ⟨t, ht⟩ := hfg
	use t; rw [← ht, Submodule.span_span_of_tower]
	theorem span_submodule_fg_of_fg {S : Submodule R M} (hS : S.FG) :
	(span A S : Submodule A M).FG := by
	obtain ⟨t, ht⟩ := hS
	use t
	rw [← ht, span_span_of_tower]

[LLaurance]

Consider having variable {S : Submodule R M}

[LLaurance]

Suggested change

	use X
	exact (Submodule.restrictScalars_span R S h (X : Set M)).symm
	exact (restrictScalars_span R A h (X : Set M)).symm
	exact ⟨X, (restrictScalars_span R A h _).symm⟩

[LLaurance]

Looks like N could be implicit

[LLaurance]

See https://github.com/leanprover-community/mathlib4/pull/33980/changes#r2723805963