den_dvd_iff — Mathlib

English

For a rational matrix A, A.den divides r if and only if every entry denominator divides r.

Русский

Для рациональной матрицы A: A.den делится на r тогда, когда каждый знаменатель A_{ij} делится на r.

LaTeX

$$$$ A^{\\mathrm{den}} \\,|\, r \\iff \\forall i,j,\\; (A_{ij}).den \\,|\\, r. $$$$

Lean4

theorem den_dvd_iff {A : Matrix m n ℚ} {r : ℕ} : A.den ∣ r ↔ ∀ i j, (A i j).den ∣ r := by simp [Matrix.den]

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