Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols
theorem Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols :
∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix m n α)
[inst_2 : Fintype m], A.transpose.HasOrthogonalRows ↔ A.HasOrthogonalCols
The theorem `Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols` states that for any matrix `A` with entries in a type `α` that supports multiplication and addition operations, and where the index type `m` for rows is finite, the transpose of `A`, denoted `Aᵀ`, has orthogonal rows if and only if `A` itself has orthogonal columns. Here, a matrix is said to have orthogonal rows (or columns) if, when considered as vectors, any two different rows (or columns) are orthogonal, i.e., their dot product is zero.
More concisely: The matrix `A` has orthogonal transpose rows if and only if it has orthogonal columns.
|
Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows
theorem Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows :
∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix m n α)
[inst_2 : Fintype n], A.transpose.HasOrthogonalCols ↔ A.HasOrthogonalRows
This theorem states that for any matrix `A` with entries in an arbitrary type `α` that supports multiplication and addition (forming a commutative monoid), indexed by arbitrary types `m` and `n`, if `n` is finite, then the transpose of `A`, denoted as `Aᵀ`, has orthogonal (perpendicular) columns if and only if `A` itself has orthogonal rows. Orthogonality here refers to the condition that the dot product of different rows (or columns in the case of the transpose) is zero.
More concisely: For a commutative monoid-valued matrix `A` of finite width `n` over an arbitrary type `α` with orthogonal rows, its transpose `Aᵀ` has orthogonal columns. Conversely, if `A` has orthogonal columns, then its transpose has orthogonal rows.
|