mathlib3

df9683ca - feat(topology/algebra/infinite_sum): lemmas about `mul_opposite` (#13674)