English
Let p ≠ 0. Then num x divides p iff there exists q ≠ 0 with x = p/q.
Русский
Пусть p ≠ 0. Тогда num x делит p тогда и только тогда, когда существует q ≠ 0 такое, что x = p/q.
LaTeX
$$$p \neq 0 \Rightarrow \operatorname{num}(x) \mid p \iff \exists q \; (q \neq 0 \land x = \dfrac{p}{q})$$$
Lean4
theorem num_dvd {x : RatFunc K} {p : K[X]} (hp : p ≠ 0) :
num x ∣ p ↔ ∃ q : K[X], q ≠ 0 ∧ x = algebraMap _ _ p / algebraMap _ _ q :=
by
constructor
· rintro ⟨q, rfl⟩
obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp
use denom x * q
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
· exact ⟨mul_ne_zero (denom_ne_zero x) hq, rfl⟩
· exact algebraMap_ne_zero hq
· rintro ⟨q, hq, rfl⟩
exact num_div_dvd p hq
