English
There exists a witness D ∈ R such that i D = i b^f.natDegree * eval(i a * bi) (f.map i) when bi i b = 1.
Русский
Существует свидетель D ∈ R такой, что i D = i b^{f.natDegree} · eval(i a · bi) (f.map i), когда bi · i b = 1.
LaTeX
$$$\exists D:\\in R, \exists \beta:\\in K, \beta \cdot i(b) = 1 \,\land \, i D = i b^{f.natDegree} \cdot eval (i a \cdot \beta) (f.map i)$$$
Lean4
/-- If `i : R → K` is a ring homomorphism, `f` is a polynomial with coefficients in `R`,
`a, b` are elements of `R`, with `i b` invertible, then there is a `D ∈ R` such that
`b ^ f.natDegree * f (a / b)` equals `i D`. -/
theorem denomsClearable_natDegree (i : R →+* K) (f : R[X]) (a : R) (bu : bi * i b = 1) :
DenomsClearable a b f.natDegree f i :=
denomsClearable_of_natDegree_le f.natDegree a bu f le_rfl
