mathlib3
49b1e35c - chore(data/countable/defs): add explanation of nolint (#17732)

Commit
3 years ago
chore(data/countable/defs): add explanation of nolint (#17732) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading