feat(Data/Complex/Basic): Adds imaginary number representation (#12427)

Adds a representation for Complex numbers and DualNumber so they can be used in #eval statements.




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/DualNumber.lean

@@ -189,4 +189,10 @@ theorem lift_inlAlgHom_eps :
   lift.apply_symm_apply <| AlgHom.id R A[ε]
 #align dual_number.lift_eps DualNumber.lift_inlAlgHom_epsₓ
 
+/-- Show DualNumber with values x and y as an "x + y*ε" string -/
+instance instRepr [Repr R] : Repr (DualNumber R) where
+  reprPrec f p :=
+    (if p > 65 then (Std.Format.bracket "(" . ")") else (·)) <|
+      reprPrec f.fst 65 ++ " + " ++ reprPrec f.snd 70 ++ "*ε"
+
 end DualNumber

Mathlib/Data/Complex/Basic.lean

@@ -941,6 +941,16 @@ theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I) := by
     mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
 #align complex.im_eq_sub_conj Complex.im_eq_sub_conj
 
+/-- Show the imaginary number ⟨x, y⟩ as an "x + y*I" string
+
+Note that the Real numbers used for x and y will show as cauchy sequences due to the way Real
+numbers are represented.
+-/
+unsafe instance instRepr : Repr ℂ where
+  reprPrec f p :=
+    (if p > 65 then (Std.Format.bracket "(" . ")") else (·)) <|
+      reprPrec f.re 65 ++ " + " ++ reprPrec f.im 70 ++ "*I"
+
 end Complex
 
 assert_not_exists Multiset

test/Complex.lean

@@ -0,0 +1,34 @@
+import Mathlib.Data.Complex.Basic
+import Mathlib.Algebra.DualNumber
+
+open DualNumber
+
+/--
+info: Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I
+-/
+#guard_msgs in
+#eval (0 : ℂ)
+
+/--
+info: Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I
+-/
+#guard_msgs in
+#eval (1 : ℂ)
+
+/--
+info: Real.ofCauchy (sorry /- 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I
+-/
+#guard_msgs in
+#eval (4 : ℂ)
+
+/--
+info: Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/)*I
+-/
+#guard_msgs in
+#eval (Complex.I : ℂ)
+
+/--
+info: Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I + (Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I)*ε
+-/
+#guard_msgs in
+#eval (0 : ℂ[ε])

test/DualNumber.lean

@@ -0,0 +1,19 @@
+import Mathlib.Algebra.DualNumber
+
+open DualNumber
+
+/-- info: 0 + 0*ε -/
+#guard_msgs in
+#eval (0 : ℕ[ε])
+
+/-- info: 2 + 0*ε -/
+#guard_msgs in
+#eval (2 : ℕ[ε])
+
+/-- info: 6 + 0*ε -/
+#guard_msgs in
+#eval (2 + 4 : ℕ[ε])
+
+/-- info: 2 + 0*ε + (0 + 0*ε)*ε -/
+#guard_msgs in
+#eval (2 : (ℕ[ε])[ε])