inner_smul_left

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#inner_smul_left

← MathLib Explorer

English

For any r in a ring with star, ⟪r x, y⟫ = r† ⟪x, y⟫.

Русский

Для любого r в кольце со звёздочкой, ⟪r x, y⟫ = r† ⟪x, y⟫.

LaTeX

$$$\langle r x, y\rangle = r^{\dagger} \langle x, y\rangle$$$

Lean4

/-- See `inner_smul_left_eq_star_smul` for the case of a general algebra action. -/
theorem inner_smul_left (x y : E) (r : 𝕜) : ⟪r • x, y⟫ = r† * ⟪x, y⟫ :=
  inner_smul_left_eq_star_smul ..

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

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

Разделы

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

Аффилиация

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