mathlib

b4d4d9aa - feat(ring_theory/algebra): more on restrict_scalars (#2445)

feat(ring_theory/algebra): more on restrict_scalars (#2445) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>