mathlib3

b19fbd79 - feat(ring_theory/algebra_tower): coefficients for a basis in an algebra tower (#4114)

feat(ring_theory/algebra_tower): coefficients for a basis in an algebra tower (#4114) This PR gives an expression for `(is_basis.smul hb hc).repr` in terms of `hb.repr` and `hc.repr`, useful if you have a field extension `L / K`, and `x y : L`, and want to write `y` in terms of the power basis of `K(x)`. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>