den_natCast — Mathlib

English

Denominator of a natural scalar embedded into a square rational matrix equals 1: den(ofNat(a) for a ∈ ℕ) = 1.

Русский

Знаменатель натурального числа, встроенного в квадратную рациональную матрицу, равен 1: den(ofNat(a)) = 1.

LaTeX

$$$\operatorname{den}\big(\operatorname{ofNat}(a)\big) = 1, \quad a \in \mathbb{N}.$$$

Lean4

@[simp]
theorem den_natCast [DecidableEq m] (a : ℕ) : (a : Matrix m m ℚ).den = 1 := by
  simpa [← diagonal_natCast] using den_map_natCast (a : Matrix m m ℕ)

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