English
Let A and B be m×n matrices over a field with an Hermitian structure. For every i and j in {1,…,m}, the inner product of the i-th row of A with the j-th row of B equals the (j,i)-entry of the product B A^H, where A^H denotes the conjugate transpose of A.
Русский
Пусть A и B — матрицы размера m×n над полем с эрмитовым сопряжением. Для любых i, j ∈ {1, …, m} скалярное произведение i-й строки A и j-й строки B равно элементу (j,i) произведения B A^H, где A^H — сопряжённо-транспонированная матрица A.
LaTeX
$$$\\\\langle A_i, B_j \\\\rangle = (B A^{\\mathrm{H}})_{j i}.$$$
Lean4
/-- The inner product of a row of `A` and a row of `B` is an entry of `B * Aᴴ`. -/
theorem inner_matrix_row_row [Fintype n] (A B : Matrix m n 𝕜) (i j : m) : ⟪A i, B j⟫ₑ = (B * Aᴴ) j i := by
simp [PiLp.inner_apply, dotProduct, mul_apply']
