inner_smul_right_eq_smul — Mathlib

English

For r in a star-ring, ⟪x, r y⟫ = r ⟪x, y⟫.

Русский

Для r в звездном кольце, ⟪x, r y⟫ = r ⟪x, y⟫.

LaTeX

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

Lean4

/-- See `inner_smul_right` for the common special when `𝕜 = 𝕝`. -/
theorem inner_smul_right_eq_smul (x y : E) (r : 𝕝) : ⟪x, r • y⟫ = r • ⟪x, y⟫ := by
  rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply, star_smul, star_star, ←
    starRingEnd_apply, inner_conj_symm]

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