addSubmonoid_closure_setOf_eq_monomial

English

Monomials generate the additive submonoid of the polynomial ring: the closure of monomials equals the whole ring.

Русский

Мономионы порождают/additive монойду полиномиального кольца: замыкание по мономионам даёт весь полиномий.

LaTeX

$$$\operatorname{AddSubmonoid}.closure\{ p \in R[X] \mid \exists n,a, p = \operatorname{monomial}(n,a) \} = \top$$$

Lean4

/-- Monomials generate the additive monoid of polynomials. -/
theorem addSubmonoid_closure_setOf_eq_monomial : AddSubmonoid.closure {p : R[X] | ∃ n a, p = monomial n a} = ⊤ :=
  by
  apply top_unique
  rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ← Finsupp.add_closure_setOf_eq_single,
    AddMonoidHom.map_mclosure]
  refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)
  rintro _ ⟨n, a, rfl⟩
  exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩

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