feat: port LinearAlgebra.Matrix.Orthogonal (#3235)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Mathlib.lean

@@ -1209,6 +1209,7 @@ import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.InvariantBasisNumber
 import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.LinearAlgebra.LinearPMap
+import Mathlib.LinearAlgebra.Matrix.Orthogonal
 import Mathlib.LinearAlgebra.Matrix.Symmetric
 import Mathlib.LinearAlgebra.Matrix.Trace
 import Mathlib.LinearAlgebra.Pi

Mathlib/LinearAlgebra/Matrix/Orthogonal.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2021 Lu-Ming Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lu-Ming Zhang
+
+! This file was ported from Lean 3 source module linear_algebra.matrix.orthogonal
+! leanprover-community/mathlib commit 790e98fbb5ec433d89d833320954607e79ae9071
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Matrix.Basic
+
+/-!
+# Orthogonal
+
+This file contains definitions and properties concerning orthogonality of rows and columns.
+
+## Main results
+
+- `matrix.HasOrthogonalRows`:
+  `A.HasOrthogonalRows` means `A` has orthogonal (with respect to `dotProduct`) rows.
+- `matrix.HasOrthogonalCols`:
+  `A.HasOrthogonalCols` means `A` has orthogonal (with respect to `dotProduct`) columns.
+
+## Tags
+
+orthogonal
+-/
+
+
+namespace Matrix
+
+variable {α n m : Type _}
+
+variable [Mul α] [AddCommMonoid α]
+
+variable (A : Matrix m n α)
+
+open Matrix
+
+/-- `A.HasOrthogonalRows` means matrix `A` has orthogonal rows (with respect to
+`Matrix.dotProduct`). -/
+def HasOrthogonalRows [Fintype n] : Prop :=
+  ∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → dotProduct (A i₁) (A i₂) = 0
+#align matrix.has_orthogonal_rows Matrix.HasOrthogonalRows
+
+/-- `A.HasOrthogonalCols` means matrix `A` has orthogonal columns (with respect to
+`Matrix.dotProduct`). -/
+def HasOrthogonalCols [Fintype m] : Prop :=
+  HasOrthogonalRows Aᵀ
+#align matrix.has_orthogonal_cols Matrix.HasOrthogonalCols
+
+/-- `Aᵀ` has orthogonal rows iff `A` has orthogonal columns. -/
+@[simp]
+theorem transpose_hasOrthogonalRows_iff_hasOrthogonalCols [Fintype m] :
+    Aᵀ.HasOrthogonalRows ↔ A.HasOrthogonalCols :=
+  Iff.rfl
+#align matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols
+
+/-- `Aᵀ` has orthogonal columns iff `A` has orthogonal rows. -/
+@[simp]
+theorem transpose_hasOrthogonalCols_iff_hasOrthogonalRows [Fintype n] :
+    Aᵀ.HasOrthogonalCols ↔ A.HasOrthogonalRows :=
+  Iff.rfl
+#align matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows
+
+variable {A}
+
+theorem HasOrthogonalRows.hasOrthogonalCols [Fintype m] (h : Aᵀ.HasOrthogonalRows) :
+    A.HasOrthogonalCols :=
+  h
+#align matrix.has_orthogonal_rows.has_orthogonal_cols Matrix.HasOrthogonalRows.hasOrthogonalCols
+
+theorem HasOrthogonalCols.transpose_hasOrthogonalRows [Fintype m] (h : A.HasOrthogonalCols) :
+    Aᵀ.HasOrthogonalRows :=
+  h
+#align matrix.has_orthogonal_cols.transpose_has_orthogonal_rows Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows
+
+theorem HasOrthogonalCols.hasOrthogonalRows [Fintype n] (h : Aᵀ.HasOrthogonalCols) :
+    A.HasOrthogonalRows :=
+  h
+#align matrix.has_orthogonal_cols.has_orthogonal_rows Matrix.HasOrthogonalCols.hasOrthogonalRows
+
+theorem HasOrthogonalRows.transpose_hasOrthogonalCols [Fintype n] (h : A.HasOrthogonalRows) :
+    Aᵀ.HasOrthogonalCols :=
+  h
+#align matrix.has_orthogonal_rows.transpose_has_orthogonal_cols Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols
+
+end Matrix