Theorem Submodule.FG.small

Modification history

2025-03-27 14:32
Mathlib/RingTheory/Finiteness/Small.lean
feat(RingTheory/Finiteness/Small): smallness properties of modules and algebras (#22911) …
Added Submodule.FG.smallView on Github →