Commit 2020-09-14 08:03 b19fbd79

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