doc(Algebra/DualNumber): notation docstrings (#7969)

Mathlib/Algebra/DualNumber.lean

@@ -39,20 +39,21 @@ Rather than duplicating the API of `TrivSqZeroExt`, this file reuses the functio
 
 variable {R : Type*}
 
-/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.-/
+/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
+`R[ε]` is notation for `DualNumber R`. -/
 abbrev DualNumber (R : Type*) : Type _ :=
   TrivSqZeroExt R R
 #align dual_number DualNumber
 
-/-- The unit element $ε$ that squares to zero. -/
+/-- The unit element $ε$ that squares to zero, with notation `ε`. -/
 def DualNumber.eps [Zero R] [One R] : DualNumber R :=
   TrivSqZeroExt.inr 1
 #align dual_number.eps DualNumber.eps
 
--- mathport name: dual_number.eps
+@[inherit_doc]
 scoped[DualNumber] notation "ε" => DualNumber.eps
 
--- mathport name: dual_number
+@[inherit_doc]
 scoped[DualNumber] postfix:1024 "[ε]" => DualNumber
 
 open DualNumber