sesqFormOfInner — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The inner product as a sesquilinear form.

Note that in the case `𝕜 = ℝ` this is a bilinear form. -/
@[simps!]
def sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
  LinearMap.mk₂'ₛₗ (RingHom.id 𝕜) (starRingEnd _) (fun x y => ⟪y, x⟫) (fun _x _y _z => inner_add_right _ _ _)
    (fun _r _x _y => inner_smul_right _ _ _) (fun _x _y _z => inner_add_left _ _ _) fun _r _x _y =>
    inner_smul_left _ _ _

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