Theorem Module.Finite.small

Modification history

2025-03-27 14:32
Mathlib/RingTheory/Finiteness/Cardinality.lean
feat(RingTheory/Finiteness/Small): smallness properties of modules and algebras (#22911) …
Modified Module.Finite.smallView on Github →
2025-01-02 11:03
Mathlib/RingTheory/Finiteness/Cardinality.lean
feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)
Added Module.Finite.smallView on Github →