transpose_mul_self_isDiag_iff_hasOrthogonalCols

English

For a finite index m, (A^T A) is diagonal if and only if A has orthogonal columns.

Русский

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

LaTeX

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

Lean4

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

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