English
The product of two canonical fractions mk' equals the canonical fraction of the product, with the expected coprimality condition preserved.
Русский
Произведение двух канонических дробей mk' равно канонической дроби произведения числителей и знаменателей с сохранением условий взаимной простоты.
LaTeX
$$$ mk' n_1 d_1 hd_1 hnd_1 \ast mk' n_2 d_2 hd_2 hnd_2 = mk' (n_1 n_2) (d_1 d_2) (Nat.mul_ne_zero hd_1 hd_2) $$$
Lean4
theorem mk'_mul_mk' (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ hd₂ hnd₁ hnd₂) (h₁₂ : n₁.natAbs.Coprime d₂)
(h₂₁ : n₂.natAbs.Coprime d₁) :
mk' n₁ d₁ hd₁ hnd₁ * mk' n₂ d₂ hd₂ hnd₂ =
mk' (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero hd₁ hd₂)
(by rw [Int.natAbs_mul]; exact (hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)) :=
by rw [mul_def]; simp [mk_eq_normalize]
