mathlib

5e9f8c1e - Lint fix: `to_additive` used in the wrong order, so it wasn't applying nolint