From 5f258eb538d15429b57cf29ce7962b14ccafc64b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 27 Oct 2023 07:19:54 +0000 Subject: [PATCH] doc(Algebra/DualNumber): notation docstrings (#7969) --- Mathlib/Algebra/DualNumber.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/DualNumber.lean b/Mathlib/Algebra/DualNumber.lean index bc4164179f383..2daaf1689615a 100644 --- a/Mathlib/Algebra/DualNumber.lean +++ b/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