den — Mathlib

English

The common denominator of a matrix with rational entries is the least common multiple of the denominators of all entries.

Русский

Общий знаменатель матрицы с рациональными элементами — наименьшее общее кратное знаменателей всех элементов.

LaTeX

$$$$ \\mathrm{den}(A) = \\mathrm{lcm}\\{ \\mathrm{den}(A_{pq}) : p,q \\} \\,.$$$$

Lean4

/-- The denominator of a matrix of rationals (as a `Nat`, defined as the LCM of the denominators of
the entries). -/
protected def den (A : Matrix m n ℚ) : ℕ :=
  Finset.univ.lcm (fun P : m × n ↦ (A P.1 P.2).den)

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