English
For any A ∈ M_n(ℚ) and indices i,j, A.num i j / A.den = A i j; i.e., the (i,j)-entry equals the numerator divided by the common denominator.
Русский
Для любой A ∈ M_n(ℚ) и индексов i,j, A.num_{ij} / A.den = A_{ij}; т.е. числитель делится на знаменатель даёт исходную запись.
LaTeX
$$$$ A^{\\mathrm{num}}_{ij} / A^{\\mathrm{den}} = A_{ij}. $$$$
Lean4
theorem num_div_den (A : Matrix m n ℚ) (i : m) (j : n) : A.num i j / A.den = A i j :=
by
obtain ⟨k, hk⟩ := den_dvd_iff.mp (dvd_refl A.den) i j
rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm, div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk,
Nat.cast_mul, ← mul_assoc, Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
