num_intCast

Mathlib.LinearAlgebra.Matrix.Integer

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

← MathLib Explorer

English

For any integer a, the numerator of its rational embedding equals a cast: (a).num = a.cast.

Русский

Числитель целого числа при его рациональном включении равен a.cast.

LaTeX

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

Lean4

@[simp]
theorem num_intCast [DecidableEq m] (a : ℤ) : (a : Matrix m m ℚ).num = a := by
  simpa [← diagonal_intCast] using num_map_intCast (a : Matrix m m ℤ)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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