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⟩