Add missing doc

leanprover-community · Feb 29, 2024 · 14b2f1f · 14b2f1f
1 parent 93a4ad1
commit 14b2f1f
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean b/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean
@@ -43,6 +43,7 @@ add_decl_doc ContinuousAlternatingMap.toContinuousMultilinearMap
 /-- Projection to `AlternatingMap`s. -/
 add_decl_doc ContinuousAlternatingMap.toAlternatingMap
 
+@[inherit_doc]
 notation M "[⋀^" ι "]→L[" R "]" N:100 => ContinuousAlternatingMap R M N ι
 
 namespace ContinuousAlternatingMap