linMulLin

Mathlib.LinearAlgebra.BilinearForm.Hom

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

← MathLib Explorer

English

Congruence with the identity in both arguments leaves the bilinear form unchanged.

Русский

Согласование по тождеству в обоих аргументах не изменяет билинейную форму.

LaTeX

$$congr (LinearEquiv.refl R M) B = B$$

Lean4

/-- `linMulLin f g` is the bilinear form mapping `x` and `y` to `f x * g y` -/
def linMulLin (f g : M →ₗ[R] R) : BilinForm R M :=
  (LinearMap.mul R R).compl₁₂ f g

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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