coe_injective

Mathlib.LinearAlgebra.BilinearForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.coe_injective

English

The map B ↦ (x,y) ↦ B(x,y) is injective on BilinForm R M.

Русский

Отображение B ↦ (x,y) ↦ B(x,y) по BilinForm R M инъективно.

LaTeX

$$$\text{If } B,D \in BilinForm\,R\,M\text{ and } (\forall x,y, B(x,y)=D(x,y)),\; B=D.$$$

Lean4

theorem coe_injective : Function.Injective ((fun B x y => B x y) : BilinForm R M → M → M → R) := fun B D h =>
  by
  ext x y
  apply congrFun₂ h

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

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

Разделы

Аффилиация

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