instRepr — Mathlib

English

There is a canonical string representation of a complex number a+bi given by the form a + b I.

Русский

Существует каноническое строковое представление числа a+bi в виде a + b I.

LaTeX

$$$\\text{repr}(a+bi) = a + b\,I$$$

Lean4

/-- 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"

Похожие утверждения