congr_fun

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

If two quadratic maps are equal, then their values coincide on every input.

Русский

Если две квадратичные карты равны, то их значения совпадают на любом входе.

LaTeX

$$$$ \\forall x, h: Q = Q' \\Rightarrow Q x = Q' x. $$$$

Lean4

theorem congr_fun (h : Q = Q') (x : M) : Q x = Q' x :=
  DFunLike.congr_fun h _

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

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

Разделы

Аффилиация

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