den_map_natCast — Mathlib

English

For a matrix with natural entries, casting to rationals yields a matrix with denominator 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{N}).$$$

Lean4

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

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