orthonormalBasisOneI_repr_symm_apply

Mathlib.Analysis.InnerProductSpace.PiL2

URI: https://scilib.ai/kg/mathlib#Complex.orthonormalBasisOneI_repr_symm_apply

← MathLib Explorer

English

The function underlying b.reindex e equals b composed with e.symm.

Русский

Функция, лежащая в основе b.reindex e, равна b ∘ e^{-1}.

LaTeX

$$$$ \\mathrm{OrthonormalBasis}.coe\\_reindex(h,b,e)=h\\circ e^{-1}. $$$$

Lean4

@[simp]
theorem orthonormalBasisOneI_repr_symm_apply (x : EuclideanSpace ℝ (Fin 2)) :
    Complex.orthonormalBasisOneI.repr.symm x = x 0 + x 1 * I :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru