inner_smul_left_eq_star_smul — Mathlib

English

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

Русский

Для элемента r из звёздной кольцевой структуры ⟪r x, y⟫ = r† ⟪x, y⟫.

LaTeX

$$$\langle r \cdot x, y\rangle = r^{\dagger} \langle x, y\rangle$$$

Lean4

/-- See `inner_smul_left` for the common special when `𝕜 = 𝕝`. -/
theorem inner_smul_left_eq_star_smul (x y : E) (r : 𝕝) : ⟪r • x, y⟫ = r† • ⟪x, y⟫ := by
  rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply, ← algebraMap_star_comm,
    ← smul_eq_mul, algebraMap_smul]

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