inner_matrix_col_col — Mathlib

English

Let A and B be m×n matrices over a field with Hermitian structure. For i,j in {1,…,n}, the inner product of the i-th column of A with the j-th column of B equals the (i,j)-entry of A^H B.

Русский

Пусть A и B — матрицы размера m×n над полем с эрмитовым сопряжением. Для i, j ∈ {1,…,n} скалярное произведение i-й и j-й столбцов A и B равно элементу (i,j) произведения A^H B.

LaTeX

$$$\\\\langle A^{T}_i, B^{T}_j \\\\rangle = (A^{\\mathrm{H}} B)_{i j}.$$$

Lean4

/-- The inner product of a column of `A` and a column of `B` is an entry of `Aᴴ * B`. -/
theorem inner_matrix_col_col [Fintype m] (A B : Matrix m n 𝕜) (i j : n) : ⟪Aᵀ i, Bᵀ j⟫ₑ = (Aᴴ * B) i j := by
  simp [PiLp.inner_apply, dotProduct, mul_apply', mul_comm]

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