Complex numbers $\mathbf{C}$ (LADR 1.1)

• Complex numbers $\mathbf{C}$ (LADR 1.1) #Card
  • 複素数の定義と、$\mathbf{C}$ 上の加法・乗法は？

Back

複素数は順序対 $(a,b)$（$a,b\in\mathbf{R}$）で、$a+bi$ と書く。 $$\mathbf{C}={a+bi : a,b\in\mathbf{R}}.$$ 加法・乗法は $$(a+bi)+(c+di)=(a+c)+(b+d)i,$$ $$(a+bi)(c+di)=(ac-bd)+(ad+bc)i.$$ $i^2=-1$ と通常の算術規則から積の公式は再導出できる（暗記不要）。

Lean

Mathlib では ℂ（Complex）。Complex.ext_iff, Complex.I_sq : I^2 = -1。