Commit 2021-09-30 11:12 09506e6c

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).