basis_repr_apply — Mathlib

English

The representation map of QuadraticAlgebra with respect to its basis sends any element to the corresponding vector of its coordinates given by its real and imaginary parts.

Русский

Карта представления квадратической алгебры относительно её базы отправляет элемент в вектор его координат, заданных действительной и мнимой частями.

LaTeX

$$$(basis\\ a\\ b).repr x = ![x.re, x.im]$$$

Lean4

@[simp]
theorem basis_repr_apply (x : QuadraticAlgebra R a b) : (basis a b).repr x = ![x.re, x.im] :=
  rfl

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