mathlib

ea94d7cd - docs(algebra/module/equiv): correct a misleading comment (#18458)

docs(algebra/module/equiv): correct a misleading comment (#18458) The linter is saying that the argument is unused because the argument is unused. The comment claiming that it doesn't appear and the linter is just confused is false. We could remove the argument, but the extra generality it would provide is illusory, and it would likely just be inconvenient. This is forward-ported in https://github.com/leanprover-community/mathlib4/pull/2347, though we will need to update the SHA again after this PR is merged.