mathlib3

d8aed79b - chore(analysis/inner_product_space/projection): Speedup `linear_isometry_equiv.reflections_generate_dim_aux` (#11443)

chore(analysis/inner_product_space/projection): Speedup `linear_isometry_equiv.reflections_generate_dim_aux` (#11443) This takes it from around 17s to around 6s on my machine. IMO using `e * f` instead of `f.trans e` makes this proof a little easier to follow, as then we don't have to translate between the two different spellings mid proof (and `prod` uses the `*` spelling internally)