inner_smul_right_real — Mathlib

English

For z ∈ ℝ, ⟪x, z y⟫ = z ⟪x, y⟫; compatibility with real scalars on second argument.

Русский

Для z ∈ ℝ выполняется ⟪x, z y⟫ = z ⟪x, y⟫; совместимость со скалярами-вещественными на втором аргументе.

LaTeX

$$$⟪x, z y⟫ = z ⟪x, y⟫$$

Lean4

@[simp]
theorem inner_smul_right_real {z : ℝ} {x y : E} : ⟪x, z • y⟫ = z • ⟪x, y⟫ :=
  by
  have h₁ : z • y = (z : ℂ) • y := by simp
  rw [h₁, ← star_inner, inner_smul_left_complex]
  simp

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