instAlgebraPolynomial — Mathlib

English

For every x in the coordinate ring, there exist polynomials p, q in R[X] such that p·1 + q·mk W' Y equals x.

Русский

Для каждого элемента x из координатного кольца существуют полиномы p, q ∈ R[X] такие, что p·1 + q·mk W' Y = x.

LaTeX

$$$\exists p\,\exists q\, (p \cdot (1 : W'.CoordinateRing) + q \cdot mk W' Y) = x$$$

Lean4

noncomputable instance : Algebra R[X] W'.CoordinateRing :=
  Quotient.algebra R[X]

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