polar_smul_left_of_tower

Mathlib.LinearAlgebra.QuadraticForm.Basic

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

← MathLib Explorer

English

For a given tower, polar (a•x) y = a • polar x y.

Русский

Для башни поляризация удовлетворяет: polar (a·x) y = a · polar x y.

LaTeX

$$polar Q (a • x) y = a • polar Q x y$$

Lean4

@[simp]
theorem polar_smul_left_of_tower (a : S) (x y : M) : polar Q (a • x) y = a • polar Q x y := by
  rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, algebraMap_smul]

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

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

Разделы

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

Аффилиация

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