English
Same divisibility property as above, expressed in simp-normal form.
Русский
Та же свойство делимости в упрощенной нормальной форме.
LaTeX
$$@[simp]\n\(\operatorname{denom}\left(\dfrac{p}{q}\right) \mid q\)$$
Lean4
@[simp]
theorem num_div_denom (x : RatFunc K) : algebraMap _ _ (num x) / algebraMap _ _ (denom x) = x := by
classical
induction x using RatFunc.induction_on with
| _ p q hq
have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq
rw [num_div p q, denom_div p hq, RingHom.map_mul, RingHom.map_mul, mul_div_mul_left, div_eq_div_iff, ←
RingHom.map_mul, ← RingHom.map_mul, mul_comm _ q, ← EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc,
mul_comm]
· apply gcd_dvd_right
· apply gcd_dvd_left
· exact algebraMap_ne_zero q_div_ne_zero
· exact algebraMap_ne_zero hq
· refine algebraMap_ne_zero (mt Polynomial.C_eq_zero.mp ?_)
exact inv_ne_zero (Polynomial.leadingCoeff_ne_zero.mpr q_div_ne_zero)
