toBilin'Aux_eq

Mathlib.LinearAlgebra.Matrix.BilinearForm

URI: https://scilib.ai/kg/mathlib#Matrix.toBilin'Aux_eq

English

The round-trip between BilinForm and Matrix toMatrix' is the identity on BilinForm.

Русский

Возврат между BilinForm и Matrix через toMatrix' дает тождественное отображение на BilinForm.

LaTeX

$$$\text{toBilin'_toMatrix'}$$$

Lean4

@[simp]
theorem toBilin'Aux_eq (M : Matrix n n R₁) : Matrix.toBilin'Aux M = Matrix.toBilin' M :=
  rfl

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

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

Разделы

Аффилиация

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