English
The map x ↦ ⟪x, y⟫_A is linear in the first argument and additive in the second; inner product on product is additive in the first argument.
Русский
Карта x ↦ ⟪x, y⟫_A линейна по первому аргументу и аддитивна по второму; внутреннее произведение на произведении аддитивно по первой компоненте.
LaTeX
$$$\\langle x+y, z \\rangle_A = \\langle x, z \\rangle_A + \\langle y, z \\rangle_A$$$
Lean4
/-- Reinterpret an inner product space `E` over `ℂ` as a `CStarModule` over `ℂ`.
Note: this instance requires `SMul ℂᵐᵒᵖ E` and `IsCentralScalar ℂ E` instances to exist on `E`,
which is unlikely to occur in practice. However, in practice one could either add those instances
to the type `E` in question, or else supply them to this instance manually, which is reason behind
the naming of these two instance arguments. -/
instance instCStarModuleComplex : CStarModule ℂ E
where
inner x y := ⟪x, y⟫_ℂ
inner_add_right := by simp [_root_.inner_add_right]
inner_self_nonneg
{x} := by
rw [← inner_self_ofReal_re, RCLike.ofReal_nonneg]
exact inner_self_nonneg
inner_self := by simp
inner_op_smul_right := by simp [inner_smul_right]
inner_smul_right_complex := by simp [inner_smul_right, smul_eq_mul]
star_inner _ _ := by simp
norm_eq_sqrt_norm_inner_self {x} := by simpa only [← inner_self_re_eq_norm] using norm_eq_sqrt_re_inner x
