English
Let x be a rational function over a field K and q a nonzero polynomial in K[X]. Then the denominator of x divides q precisely when x can be written as the quotient of two polynomials by the same denominator, i.e. x = p/q for some p ∈ K[X].
Русский
Пусть x - рациональная функция над полем K, и q — ненулевой многочлен из K[X]. Тогда знаменатель x делится на q тогда и только если существует p ∈ K[X], такое что x = p/q.
LaTeX
$$$\\denom(x) \\mid q \\;\\Longleftrightarrow\\; \\exists p \\in K[X],\\; x = \\text{algebraMap } p / \\text{algebraMap } q$$$
Lean4
theorem denom_dvd {x : RatFunc K} {q : K[X]} (hq : q ≠ 0) :
denom x ∣ q ↔ ∃ p : K[X], x = algebraMap _ _ p / algebraMap _ _ q :=
by
constructor
· rintro ⟨p, rfl⟩
obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq
use num x * p
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
exact algebraMap_ne_zero hp
· rintro ⟨p, rfl⟩
exact denom_div_dvd p q
