English
For any x, (−x).num · x.denom = −x.num · (−x).denom, showing compatibility with negation.
Русский
Для любого x выполняется (−x).num · x.denom = −x.num · (−x).denom, что согласуется с отрицанием.
LaTeX
$$$(-x).num \cdot x.denom = -x.num \cdot (-x).denom$$$
Lean4
theorem num_denom_add (x y : RatFunc K) :
(x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * 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]
rw [div_add_div, RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul]
· exact algebraMap_ne_zero (denom_ne_zero x)
· exact algebraMap_ne_zero (denom_ne_zero y)
