mathlib3

142f0017 - chore(cmd/where): remove unused argument (#2486)

chore(cmd/where): remove unused argument (#2486) Just remove an unused argument from the `#where` declaration, satisfying the linter. <br> <br> <br>