doc(algebra/module/linear_map): Explain where the ring instance is (#…

…5023) Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Nov 18, 2020 · d22a878 · d22a878
1 parent dfdad99
commit d22a878
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
@@ -273,7 +273,8 @@ end add_comm_group
 
 end is_linear_map
 
-/-- Ring of linear endomorphismsms of a module. -/
+/-- Linear endomorphisms of a module, with associated ring structure
+`linear_map.endomorphism_semiring` and algebra structure `module.endomorphism_algebra`. -/
 abbreviation module.End (R : Type u) (M : Type v)
   [semiring R] [add_comm_monoid M] [semimodule R M] := M →ₗ[R] M