num_map_natCast — Mathlib

English

Casting natural entries to rationals preserves the numerator: (A.map (↑)).num = A.map (↑) for A : M_{m×n}(ℕ).

Русский

Преобразование натуральных чисел в рациональные числа сохраняет числитель: (A.map ↑).num = A.map ↑ для A : M_{m×n}(ℕ).

LaTeX

$$$\operatorname{num}(A^{\uparrow}) = A^{\uparrow}, \quad A \in M_{m \times n}(\mathbb{N}).$$$

Lean4

@[simp]
theorem num_map_natCast (A : Matrix m n ℕ) : (A.map (↑)).num = A.map (↑) := by simp [Matrix.num, Function.comp_def]

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