den_map_intCast — Mathlib

English

If A has integer entries, then casting to rationals yields a matrix whose denominator is 1: den(A.map ↑) = 1 for A : M_{m×n}(ℤ).

Русский

Если матрица имеет целочисленные элементы, то их приведение к рациональным числам дает матрицу с знаменателем 1: den(A.map ↑) = 1 для A : M_{m×n}(ℤ).

LaTeX

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

Lean4

@[simp]
theorem den_map_intCast (A : Matrix m n ℤ) : (A.map (↑)).den = 1 := by simp [← Nat.dvd_one, Matrix.den_dvd_iff]

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