mathlib

09506e6c - feat(ring_theory/finiteness): add finiteness of restrict_scalars (#9363)

feat(ring_theory/finiteness): add finiteness of restrict_scalars (#9363) We add `module.finitte.of_restrict_scalars_finite` and related lemmas: if `A` is an `R`-algebra and `M` is an `A`-module that is finite as `R`-module, then it is finite as `A`-module (similarly for `finite_type`).