Theorem Submodule.FG.restrictScalars_of_surjective

Modification history

2026-02-01 13:22
Mathlib/RingTheory/Finiteness/Basic.lean
feat(RingTheory/Finiteness/Basic): add lemmas for restricting scalars (#33980) …
Added Submodule.FG.restrictScalars_of_surjectiveView on Github →