coe_inner — Mathlib

English

The inner product on a subspace equals the ambient inner product after embedding into the larger space.

Русский

Укрупненное вложение подпространства сохраняет скалярное произведение: ⟪x,y⟫_W = ⟪x,y⟫_E.

LaTeX

$$$\langle x,y\rangle_W = \langle x,y\rangle_E \quad (x,y \in W)$$$

Lean4

/-- The inner product on submodules is the same as on the ambient space. -/
@[simp]
theorem coe_inner (W : Submodule 𝕜 E) (x y : W) : ⟪x, y⟫ = ⟪(x : E), ↑y⟫ :=
  rfl

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