Commit 2026-02-01 13:22 c8e5e598

feat(RingTheory/Finiteness/Basic): add lemmas for restricting scalars (#33980) 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
• FG.span_submodule 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
• changing some submodule / ring hypotheses to implicit