mathlib

657cfeb6 - doc(algebra/polynomial/big_operators): add / fix docstrings and lint (#5950)