Theorem Algebra.FiniteType.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 Algebra.FiniteType.smallView on Github →