English
For x, y, the numerator of their product satisfies (x*y).num · (denom x · denom y) = (num x · num y) · (denom(x*y)).
Русский
Для x и y числитель произведения удовлетворяет формуле: (x*y).num·(denom x · denom y) = (num x · num y) · (denom(x*y)).
LaTeX
$$$\operatorname{num}(x\cdot y) \cdot (\operatorname{denom}(x) \cdot \operatorname{denom}(y)) = (\operatorname{num}(x) \cdot \operatorname{num}(y)) \cdot \operatorname{denom}(x\cdot y)$$$
Lean4
theorem num_denom_mul (x y : RatFunc K) : (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom :=
(num_mul_eq_mul_denom_iff (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))).mpr <| by
conv_lhs => rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← RingHom.map_mul, ← RingHom.map_mul]
