Theorem Set.Finite.submoduleSpan

Modification history

2024-10-17 15:04
Mathlib/RingTheory/Finiteness.lean
feat: Over a finite ring, a module is finite iff it is finite dimensional (#17707) …
Added Set.Finite.submoduleSpanView on Github →