Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 leanprover-community/mathlib4#2347, though we will need to update the SHA again after this PR is merged.
- Loading branch information