equivProd — Mathlib

English

There is a natural equivalence between quadratic algebras QA(R; a,b) and the product R×R, mapping an element to its real and imaginary parts and vice versa.

Русский

Существует естественное эквивалентное отображение между квадратической алгеброй QA(R; a,b) и произведением R×R, переходящее от элемента к его действительной и мнимой частям и обратно.

LaTeX

$$$QA(R;a,b) \\simeq R \\times R.$$$

Lean4

/-- The equivalence between quadratic algebra over `R` and `R × R`. -/
@[simps symm_apply]
def equivProd (a b : R) : QuadraticAlgebra R a b ≃ R × R
    where
  toFun z := (z.re, z.im)
  invFun p := ⟨p.1, p.2⟩

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