Mention notation in docstrings

Mathlib/LinearAlgebra/Alternating/Basic.lean

@@ -64,8 +64,8 @@ section
 
 variable (R M N ι)
 
-/-- An alternating map is a multilinear map that vanishes when two of its arguments are equal.
--/
+/-- An alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→ₗ[R] N`,
+is a multilinear map that vanishes when two of its arguments are equal. -/
 structure AlternatingMap extends MultilinearMap R (fun _ : ι => M) N where
   /-- The map is alternating: if `v` has two equal coordinates, then `f v = 0`. -/
   map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toFun v = 0

Mathlib/Topology/Algebra/Module/Alternating/Basic.lean

@@ -27,7 +27,8 @@ open Function Matrix
 
 open scoped BigOperators
 
-/-- A continuous alternating map is a continuous map from `ι → M` to `N` that is
+/-- A continuous alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→L[R] N`,
+is a continuous map that is
 
 - multilinear : `f (update m i (c • x)) = c • f (update m i x)` and
   `f (update m i (x + y)) = f (update m i x) + f (update m i y)`;