exists_image_comap_of_monic — Mathlib

English

If f and g are polynomials with g monic, there exists a finite t such that comap along C of the difference Z(g) \\ Z(f) is the complement of Z(t).

Русский

Если f и g — многочлены, причём g монический, существует конечное множество t так, что comap C '' (Z(g) \\ Z(f)) = Z(t)^c.

LaTeX

$$$\\exists t:\\mathrm{Finset}\\ R,\\ \\mathrm{comap}\\ C '' (Z(g) \\setminus Z(f)) = (Z(t))^c$$$

Lean4

theorem exists_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
    ∃ t : Finset R, comap C '' (zeroLocus { g } \ zeroLocus { f }) = (zeroLocus t)ᶜ :=
  by
  apply (config := { allowSynthFailures := true }) exists_image_comap_of_finite_of_free
  · exact .of_basis (AdjoinRoot.powerBasis' hg).basis
  · exact .of_basis (AdjoinRoot.powerBasis' hg).basis

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