den_transpose — Mathlib

English

For any rational matrix A, the common denominator remains the same after transposition: den(A^T) = den(A).

Русский

Для любой рациональной матрицы A общая знаменатель остается неизменным после транспонирования: den(A^T) = den(A).

LaTeX

$$$\operatorname{den}(A^T) = \operatorname{den}(A), \quad A \in M_{m \times n}(\mathbb{Q}).$$$

Lean4

@[simp]
theorem den_transpose (A : Matrix m n ℚ) : (Aᵀ).den = A.den :=
  eq_of_forall_dvd fun _ ↦ by simpa [den_dvd_iff] using forall_comm

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