exists_smul_basis_eq — Mathlib

English

There exists p, q ∈ R[X] such that p•1 + q•mk W' Y equals any given x in the coordinate ring.

Русский

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

LaTeX

$$∃ p q ∈ R[X], p•1 + q•mk W' Y = x$$

Lean4

theorem exists_smul_basis_eq (x : W'.CoordinateRing) : ∃ p q : R[X], p • (1 : W'.CoordinateRing) + q • mk W' Y = x :=
  by
  have h := (CoordinateRing.basis W').sum_equivFun x
  rw [Fin.sum_univ_succ, Fin.sum_univ_one, basis_zero, Fin.succ_zero_eq_one, basis_one] at h
  exact ⟨_, _, h⟩

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