transpose_mem_matrix_iff

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.transpose_mem_matrix_iff

English

For any matrix M, M^T ∈ S.matrix iff M ∈ S.matrix.

Русский

Для любой матрицы M верно, что M^T ∈ S.matrix тогда и только тогда, когда M ∈ S.matrix.

LaTeX

$$$M^{\\top} \\in S.matrix \\iff M \\in S.matrix$$$

Lean4

@[simp]
theorem transpose_mem_matrix_iff {M : Matrix m n α} : Mᵀ ∈ S.matrix ↔ M ∈ S.matrix :=
  forall_comm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru