map_add₂

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.map_add₂

English

For any bilinear map f, f(r·x, y) = ρ r · f(x, y).

Русский

Для билинейного отображения f: f(r·x, y) = ρ(r) · f(x, y).

LaTeX

$$$ f(r\\cdot x, y) = ρ(r) \\cdot f(x, y) $$$

Lean4

theorem map_add₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
  (flip f y).map_add _ _

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

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

Разделы

Аффилиация

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