mathlib3

f34fa5fc - feat(algebra/algebra/subalgebra): use opt_param for redundant axioms (#6417)