num_ofNat

Mathlib.LinearAlgebra.Matrix.Integer

URI: https://scilib.ai/kg/mathlib#Matrix.num_ofNat

English

Numerator of the matrix corresponding to a Nat via ofNat equals the Nat cast to rationals: (ofNat(a)).num = a.cast.

Русский

Числитель матрицы, соответствующей a через ofNat, равен a.cast.

LaTeX

$$$\operatorname{num}(\operatorname{ofNat}(a)) = a^{\uparrow}, \ a \in \mathbb{N}.$$$

Lean4

@[simp]
theorem num_ofNat [DecidableEq m] (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : Matrix m m ℚ).num = a :=
  num_natCast a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru