transpose_mul — Mathlib

English

For A ∈ M_{m×n}(α) and N ∈ M_{n×l}(α), (MN)ᵀ = Nᵀ Mᵀ, i.e., transpose commutes with matrix multiplication up to the reverse order.

Русский

Для матриц A и N верно (AN)ᵀ = Nᵀ Aᵀ, т. е. транспонирование сохраняет произведение с перестановкой порядков.

LaTeX

$$$(MN)^{\\top} = N^{\\top} M^{\\top}$$$

Lean4

@[simp]
theorem transpose_mul [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix m n α) (N : Matrix n l α) :
    (M * N)ᵀ = Nᵀ * Mᵀ := by
  ext
  apply dotProduct_comm

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