Commit 2025-03-27 14:32 d6403f93

View on Github →

feat(RingTheory/Finiteness/Small): smallness properties of modules and algebras (#22911) Basic smallness properties (with respect to universe) for modules and algebras.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/DFinsupp/Small.lean

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

deleted theorem Module.Finite.small

Created Mathlib/RingTheory/Finiteness/Small.lean

added theorem Algebra.FiniteType.small

added theorem Module.Finite.small

added theorem Subalgebra.FG.small

added theorem Submodule.FG.small

added theorem Submodule.small_span

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean