den_intCast — Mathlib

English

For any DecidableEq m, integer a embedded into a rational matrix has denominator 1: den(a) = 1.

Русский

Для любого DecidableEq m целое a, встроенное в рациональную матрицу, имеет знаменатель 1: den(a) = 1.

LaTeX

$$$\operatorname{den}(a) = 1, \ a \in \mathbb{Z}, \ [\text{DecidableEq } m].$$$

Lean4

@[simp]
theorem den_intCast [DecidableEq m] (a : ℤ) : (a : Matrix m m ℚ).den = 1 := by
  simpa [← diagonal_intCast] using den_map_intCast (a : Matrix m m ℤ)

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