gram_single — Mathlib

English

The Gram matrix of a single vector v_i = x placed at index i is the scalar ⟪x,x⟫ placed on the (i,i) position, with zeros elsewhere.

Русский

Граммовая матрица одного вектора v_i = x имеет на диагонали элемент ⟪x,x⟫, а остальные элементы равны нулю.

LaTeX

$$$ \ gram 𝕜 (\Pi.single i x) = \mathrm{Matrix.single } i i \langle x, x \rangle_{𝕜} $$$

Lean4

@[simp]
theorem gram_single [DecidableEq n] (i : n) (x : E) : gram 𝕜 (Pi.single i x) = Matrix.single i i ⟪x, x⟫_𝕜 :=
  by
  ext j k
  obtain hij | rfl := ne_or_eq i j
  · simp [hij]
  obtain hik | rfl := ne_or_eq i k
  · simp [hik]
  simp

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