English
For any RatFunc x and y over a field K, the numerator of the product x·y divides the product of the numerators: num(xy) ∣ num(x)·num(y).
Русский
Для любых рациональных функций x и y над полем K, число-числитель произведения x·y делится на произведение числителей: num(xy) делит num(x)·num(y).
LaTeX
$$$\\operatorname{num}(x\\cdot y) \\mid \\operatorname{num}(x) \\cdot \\operatorname{num}(y)$$$
Lean4
theorem num_mul_dvd (x y : RatFunc K) : num (x * y) ∣ num x * num y :=
by
by_cases hx : x = 0
· simp [hx]
by_cases hy : y = 0
· simp [hy]
rw [num_dvd (mul_ne_zero (num_ne_zero hx) (num_ne_zero hy))]
refine ⟨x.denom * y.denom, mul_ne_zero (denom_ne_zero x) (denom_ne_zero y), ?_⟩
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
