transpose_hasOrthogonalRows_iff_hasOrthogonalCols

English

Addition of 3-element vectors is performed componentwise.

Русский

Сложение векторов длины 3 выполняется по компонентам.

LaTeX

$$$\begin{pmatrix} a_0 \\ a_1 \\ a_2 \end{pmatrix} + \begin{pmatrix} b_0 \\ b_1 \\ b_2 \end{pmatrix} = \begin{pmatrix} a_0 + b_0 \\ a_1 + b_1 \\ a_2 + b_2 \end{pmatrix}$$$

Lean4

/-- `Aᵀ` has orthogonal rows iff `A` has orthogonal columns. -/
@[simp]
theorem transpose_hasOrthogonalRows_iff_hasOrthogonalCols [Fintype m] : Aᵀ.HasOrthogonalRows ↔ A.HasOrthogonalCols :=
  Iff.rfl

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