ext — Mathlib

English

If two complex numbers have the same real part and the same imaginary part, then they are equal.

Русский

Если две комплексные числа имеют одинаковые действительную и мнимую части, то они равны.

LaTeX

$$$$\forall z,w \in \mathbb{C},\ \operatorname{Re}(z) = \operatorname{Re}(w) \land \operatorname{Im}(z) = \operatorname{Im}(w) \Rightarrow z = w.$$$$

Lean4

theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
  | ⟨_, _⟩, ⟨_, _⟩, rfl, rfl => rfl

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