inner_sub_left

Mathlib.Analysis.CStarAlgebra.Module.Defs

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

English

For all x, y, z in E, ⟪x − y, z⟫ = ⟪x, z⟫ − ⟪y, z⟫.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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