mul_transpose_self_isDiag_iff_hasOrthogonalRows

English

For a finite index n, the matrix A has (A A^T) diagonal if and only if rows of A are orthogonal.

Русский

Для конечного n матрица A имеет диагональность A A^T тогда и только тогда, когда строки A попарно ортогональны.

LaTeX

$$$\\forall {\\alpha} {n} {m} [Fintype n] [Mul \\alpha] [AddCommMonoid \\alpha] {A : Matrix m n \\alpha}, (A * A^T).IsDiag \\iff A.HasOrthogonalRows$$$

Lean4

theorem mul_transpose_self_isDiag_iff_hasOrthogonalRows [Fintype n] [Mul α] [AddCommMonoid α] {A : Matrix m n α} :
    (A * Aᵀ).IsDiag ↔ A.HasOrthogonalRows :=
  Iff.rfl

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