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

eric-wieser · eric-wieser · commit ea94d7cd54ad · 2023-02-27T00:20:09.000Z
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.
diff --git a/src/algebra/module/equiv.lean b/src/algebra/module/equiv.lean
@@ -240,7 +240,8 @@ variables (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ
 
 include σ₃₁
 /-- Linear equivalences are transitive. -/
--- Note: The linter thinks the `ring_hom_comp_triple` argument is doubled -- it is not.
+-- Note: the `ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
+-- implicitly for lemmas like `linear_equiv.self_trans_symm`.
 @[trans, nolint unused_arguments]
 def trans : M₁ ≃ₛₗ[σ₁₃] M₃ :=
 { .. e₂₃.to_linear_map.comp e₁₂.to_linear_map,
