inner_smul_right

Mathlib.Analysis.InnerProductSpace.Defs

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.Core.inner_smul_right

← MathLib Explorer

English

For all x,y and r, ⟪x, r y⟫ = r ⟪x,y⟫.

Русский

Для всех x, y и r: ⟨x, r y⟩ = r ⟨x,y⟩.

LaTeX

$$$\\\\langle x, r y \\\\rangle = r \\\\langle x, y \\\\rangle$$$

Lean4

theorem inner_smul_right (x y : F) {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ :=
  by
  rw [← inner_conj_symm, inner_smul_left]
  simp only [conj_conj, inner_conj_symm, RingHom.map_mul]

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

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

Разделы

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

Аффилиация

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