denomsClearable_of_natDegree_le — Mathlib

English

If f has natDegree ≤ N, then DenomsClearable a b N f i holds.

Русский

Если natDegree f ≤ N, то DenomsClearable a b N f i выполняется.

LaTeX

$$$\forall f:\; \mathrm{natDegree}(f) \le N \rightarrow DenomsClearable\ a\ b\ N\ f\ i$$$

Lean4

theorem denomsClearable_of_natDegree_le (N : ℕ) (a : R) (bu : bi * i b = 1) :
    ∀ f : R[X], f.natDegree ≤ N → DenomsClearable a b N f i :=
  induction_with_natDegree_le _ N (denomsClearable_zero N a bu) (fun _ r _ => denomsClearable_C_mul_X_pow a bu r)
    fun _ _ _ _ df dg => df.add dg

Похожие утверждения