Theorem Submodule.FG.of_restrictScalars

Modification history

2026-02-01 13:22
Mathlib/RingTheory/Finiteness/Basic.lean
feat(RingTheory/Finiteness/Basic): add lemmas for restricting scalars (#33980) …
Modified Submodule.FG.of_restrictScalarsView on Github →
2025-04-08 21:08
Mathlib/RingTheory/Finiteness/Basic.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified Submodule.FG.of_restrictScalarsView on Github →
2024-11-25 08:40
Mathlib/RingTheory/Finiteness/Basic.lean
feat: the free locus of a (finitely presented) module (#18691)
Added Submodule.FG.of_restrictScalarsView on Github →