linearEquivTuple_apply — Mathlib

English

For any element z ∈ QuadraticAlgebra R a b, the coordinate map (linearEquivTuple a b) sends z to the two-component vector (z.re, z.im).

Русский

Для любого элемента z из QuadraticAlgebra R a b отображение координат (linearEquivTuple a b) отправляет z в вектор (z.re, z.im).

LaTeX

$$$ (linearEquivTuple a b) z = ![z.re, z.im] $$$

Lean4

@[simp]
theorem linearEquivTuple_apply (z : QuadraticAlgebra R a b) : (linearEquivTuple a b) z = ![z.re, z.im] :=
  rfl

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