Theorem Submodule.FG.of_finite

Modification history

2026-01-11 14:20

Mathlib/RingTheory/Finiteness/Basic.lean

chore: tidy results around `Module.Finite` (#33614) …

Added Submodule.FG.of_finite View on Github →