mathlib3

[Merged by Bors] - chore(scripts): update nolints.txt

#19227

Closed