mathlib

b351ca98 - chore(algebra/algebra/tower): golf ext lemma (#10756)

chore(algebra/algebra/tower): golf ext lemma (#10756) It turns out that we have both `algebra.ext` and `algebra.algebra_ext`, with slightly different statements. This changes one to be proved in terms of the other.