English
DenomsClearable is closed under addition: if f and g admit denominator clearing with respect to a, b, N, then f + g does as well.
Русский
DenomsClearable сохраняется при сложении: если f и g допускают очистку знаменателей относительно a, b, N, то и f+g допускает.
LaTeX
$$$\forall f,g:\; DenomsClearable\ a\ b\ N\ f\ i \land DenomsClearable\ a\ b\ N\ g\ i \rightarrow DenomsClearable\ a\ b\ N\ (f+g)\ i$$$
Lean4
theorem add {N : ℕ} {f g : R[X]} :
DenomsClearable a b N f i → DenomsClearable a b N g i → DenomsClearable a b N (f + g) i :=
fun ⟨Df, bf, bfu, Hf⟩ ⟨Dg, bg, bgu, Hg⟩ =>
⟨Df + Dg, bf, bfu, by
rw [RingHom.map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
congr
refine @inv_unique K _ (i b) bg bf ?_ ?_ <;> rwa [mul_comm]⟩
