coe_copy

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

English

The simplified coercion of a copied QuadraticMap equals the new function.

Русский

Упрощённое приведение копированной квадратичной карты равно новой функции.

LaTeX

$$$$ \\operatorname{coe}(Q.copy Q' h) = Q'. $$$$

Lean4

@[simp]
theorem coe_copy (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : ⇑(Q.copy Q' h) = Q' :=
  rfl

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

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

Разделы

Аффилиация

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