Environment linters should remind users how to disable them

[bryangingechen]

Similarly to how syntax linters in Lean core do it: https://github.com/leanprover/lean4/blob/206eb73cd9de4b58abbb2eae20a41fd9b7af187b/src/Lean/Linter/Basic.lean#L75

The relevant code seems to be at: https://github.com/leanprover-community/batteries/blob/6f7d05f4955eb5af9799d828b697251bb2c9c0b8/Batteries/Tactic/Lint/Frontend.lean#L194

cf. #FLT > unused argument linter issue @ 💬

(It might also be good for the documentation of environment linters to mention the term "environment linter" and disucss the distinction with "syntax linters" as well).