Theorem Module.Finite.of_restrictScalars_finite
Modification history
2025-04-08 21:08
Mathlib/RingTheory/Finiteness/Basic.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified Module.Finite.of_restrictScalars_finiteView on Github →2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Module.Finite.of_restrictScalars_finiteView on Github →