mathlib

e89222a6 - feat(algebra/module,linear_algebra): some `restrict_scalars` lemmas (#12181)

feat(algebra/module,linear_algebra): some `restrict_scalars` lemmas (#12181) * add `linear_map.coe_restrict_scalars` (demoting `linear_map.restrict_scalars_apply` from `simp` lemma) * add `submodule.restrict_scalars_eq_top_iff` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>