English
For any N, a, b, with bi · i b = 1, and for any n ≤ N, r ∈ R, the polynomial C r · X^n also admits a denominator clearing witness.
Русский
Для любых N, a, b с bi · i(b) = 1 и любого n ≤ N, a polynomial C r · X^n также допускает очистку знаменателей.
LaTeX
$$$\forall N\; (a)\; (bu)\; (n)\; (r)\; (n\le N) \rightarrow DenomsClearable\ a\ b\ N\ (C r \cdot X^n)\ i$$$
Lean4
theorem denomsClearable_C_mul_X_pow {N : ℕ} (a : R) (bu : bi * i b = 1) {n : ℕ} (r : R) (nN : n ≤ N) :
DenomsClearable a b N (C r * X ^ n) i :=
by
refine ⟨r * a ^ n * b ^ (N - n), bi, bu, ?_⟩
rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, eval_X, mul_comm]
rw [← tsub_add_cancel_of_le nN]
conv_lhs => rw [← mul_one (i a), ← bu]
simp [mul_assoc, mul_comm, mul_left_comm, pow_add, mul_pow]
