English
For any a ∈ ℚ, m ∈ M, s ∈ ℕ+, the action of a on mk(m,s) is mk(a.num · m, (a.den, a.den_pos) · s).
Русский
Для любых $a\\in\\mathbb{Q}$, $m\\in M$, $s\\in\\mathbb{N}_{>0}$ выполняется действие $a$ на $\\mathrm{mk}(m,s)$ равняется $\\mathrm{mk}(a.num \\cdot m, (a.den, a.den_pos) \\cdot s)$.
LaTeX
$$$a\\cdot \\mathrm{mk}(m,s) = \\mathrm{mk}(a.num\\cdot m, \\langle a.den, a.den_pos\\rangle \\cdot s)$$$
Lean4
theorem qsmul_mk (a : ℚ) (m : M) (s : ℕ+) : a • mk m s = mk (a.num • m) (⟨a.den, a.den_pos⟩ * s) :=
by
obtain h | h := le_total 0 a
· rw [qsmul_of_nonneg h, nnqsmul_mk, ← natCast_zsmul]
congr
simpa using h
· rw [qsmul_of_nonpos h]
have : a.num.natAbs • m = -a.num • m := by
rw [← natCast_zsmul]
congr
simpa using h
simp [nnqsmul_mk, this, ← neg_mk]
