mathlib3

a225e12c - feat(linear_algebra/basic): add is_scalar_tower instance for hom type (#6331)

feat(linear_algebra/basic): add is_scalar_tower instance for hom type (#6331) This instance tells Lean that if R is an S-algebra with R and S both commutative semirings, then the R-action on Hom_R(M,N) is compatible with the S-action. `linear_map.is_scalar_tower_extend_scalars` is just a special case of this new instance with the `smul_comm_class` arguments populated with `is_scalar_tower.to_smul_comm_class` and `smul_comm_class_self`, so has been removed. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>