polynomials spanned by monomials

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is something along these lines already in mathlib? Thanks!

import data.polynomial.basic

variables {R : Type*} [semiring R] {r : R}

open polynomial finset

lemma polynomial.add_submonoid_closure_monomial_eq_top :
  add_submonoid.closure { m : polynomial R | ∃ n a, m = monomial n a} = ⊤ :=
sorry

[Eric Wieser]

I think I've seen something similar, but I think it was about add_monoid_algebra and single, and possibly also submodule

[Riccardo Brasca]

I am with my phone so I it's difficult to search the library, but there is something like this in finsupp

[Damiano Testa]

Ok, thank you for your answers: I will keep looking!