ext_iff — Mathlib

English

Two quaternions are equal if and only if their real parts are equal and their imaginary parts are equal.

Русский

Два кватерниона равны тогда и только тогда, когда равны их действительная и мнимая части.

LaTeX

$$$z = w \iff \mathrm{re}(z) = \mathrm{re}(w) \land \mathrm{im}(z) = \mathrm{im}(w)$$$

Lean4

theorem ext_iff {z w : K} : z = w ↔ re z = re w ∧ im z = im w :=
  ⟨fun h => h ▸ ⟨rfl, rfl⟩, fun ⟨h₁, h₂⟩ => re_add_im z ▸ re_add_im w ▸ h₁ ▸ h₂ ▸ rfl⟩

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