inner_sub_right

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.inner_sub_right

English

For all x, y, z in E, ⟨x, y - z⟩ = ⟨x, y⟩ - ⟨x, z⟩.

Русский

Для любых x, y, z в E: ⟨x, y − z⟩ = ⟨x, y⟩ − ⟨x, z⟩.

LaTeX

$$$\\\\langle x, y - z \\\\rangle_A =\\\\langle x, y \\\\rangle_A - \\\\langle x, z \\\\rangle_A$$$

Lean4

@[simp]
theorem inner_sub_right {x y z : E} : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ := by simp [← innerₛₗ_apply]

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

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

Разделы

Аффилиация

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