toBilin_toMatrix

Mathlib.LinearAlgebra.Matrix.BilinearForm

URI: https://scilib.ai/kg/mathlib#Matrix.toBilin_toMatrix

English

Applying BilinForm.toMatrix to Matrix.toBilin yields the original bilinear form.

Русский

Применение BilinForm.toMatrix к Matrix.toBilin восстанавливает исходную билинейную форму.

LaTeX

$$Matrix.toBilin b (BilinForm.toMatrix b B) = B$$

Lean4

@[simp]
theorem toBilin_toMatrix (B : BilinForm R₁ M₁) : Matrix.toBilin b (BilinForm.toMatrix b B) = B :=
  (Matrix.toBilin b).apply_symm_apply B

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

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

Разделы

Аффилиация

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