diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean b/Mathlib/Topology/Algebra/Module/Alternating/Basic.lean index e25ac77c99a0e..6180e771b20a3 100644 --- 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