English
DenomsClearable formalizes the property that b^N f(a/b) has no denominators, given a suitable map i and a relation between a, b, and the image under i.
Русский
DenomsClearable формализует свойство отсутствия знаменателей в b^N f(a/b) при подходящей карте i и соотношениях между a, b и образом через i.
LaTeX
$$$\exists (D:\, R) (\, \beta : K), \beta \cdot i(b) = 1 \land i D = i b^N \cdot eval (i a \cdot \beta) (f.map i)$$$
Lean4
/-- `denomsClearable` formalizes the property that `b ^ N * f (a / b)`
does not have denominators, if the inequality `f.natDegree ≤ N` holds.
The definition asserts the existence of an element `D` of `R` and an
element `bi = 1 / i b` of `K` such that clearing the denominators of
the fraction equals `i D`.
-/
def DenomsClearable (a b : R) (N : ℕ) (f : R[X]) (i : R →+* K) : Prop :=
∃ (D : R) (bi : K), bi * i b = 1 ∧ i D = i b ^ N * eval (i a * bi) (f.map i)
