toFun_eq_coe

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.toFun_eq_coe

English

The canonical coercion from QuadraticMap to functions is identical to its toFun field.

Русский

Каноническое приведение из QuadraticMap к функциям совпадает с полем toFun.

LaTeX

$$$$ Q.toFun = \\; \\operatorname{coe} Q. $$$$

Lean4

/-- The `simp` normal form for a quadratic map is `DFunLike.coe`, not `toFun`. -/
@[simp]
theorem toFun_eq_coe : Q.toFun = ⇑Q :=
  rfl

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

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

Разделы

Аффилиация

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