Theorem Submodule.FG.restrictScalars

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 View on Github →