BilinMap

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinMap

English

A BilinForm is a BilinMap from M to R, i.e., a bilinear form valued in the base ring.

Русский

BilinForm — билинейная форма на пространстве M со значением в базе R.

LaTeX

$$$$BilinForm\, :\; R \to \text{(M →ₗ[R] M →ₗ[R] R)}.$$$$

Lean4

/-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`. -/
protected abbrev BilinMap : Type _ :=
  M →ₗ[R] M →ₗ[R] Nₗ

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

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

Разделы

Аффилиация

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