mathlib

5cd3c253 - chore(algebra/ring/equiv): split out results about big operators (#17750)