feat(/analysis/inner_product_space/pi_L2): inner_matrix_row_row (#1…

…2177)

The inner product between rows/columns of matrices.

src/analysis/inner_product_space/pi_L2.lean

@@ -381,3 +381,23 @@ def linear_isometry_equiv.from_orthogonal_span_singleton
   (n : ℕ) [fact (finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
   (𝕜 ∙ v)ᗮ ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
 linear_isometry_equiv.of_inner_product_space (finrank_orthogonal_span_singleton hv)
+
+section matrix
+
+open_locale matrix
+
+variables {n m : ℕ}
+
+local notation `⟪`x`, `y`⟫ₘ` := @inner 𝕜 (euclidean_space 𝕜 (fin m)) _ x y
+local notation `⟪`x`, `y`⟫ₙ` := @inner 𝕜 (euclidean_space 𝕜 (fin n)) _ x y
+
+/-- The inner product of a row of A and a row of B is an entry of B ⬝ Aᴴ. -/
+lemma inner_matrix_row_row (A B : matrix (fin n) (fin m) 𝕜) (i j : (fin n)) :
+  ⟪A i, B j⟫ₘ = (B ⬝ Aᴴ) j i := by {simp only [inner, matrix.mul_apply, star_ring_end_apply,
+    matrix.conj_transpose_apply,mul_comm]}
+
+/-- The inner product of a column of A and a column of B is an entry of Aᴴ ⬝ B -/
+lemma inner_matrix_col_col (A B : matrix (fin n) (fin m) 𝕜) (i j : (fin m)) :
+  ⟪Aᵀ i, Bᵀ j⟫ₙ = (Aᴴ ⬝ B) i j := rfl
+
+end matrix