R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ span R (of' R M '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ f ∈ adjoin R (of' R M '' ↑f.support)
suffices span R (of' R M '' f.support) ≤
    Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
  exact this (mem_span_support f)
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ of' R M '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ span R (of' R M '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
rw [Submodule.span_le]
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ of' R M '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))
exact subset_adjoin
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
this : span R (of' R M '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
⊢ f ∈ adjoin R (of' R M '' ↑f.support)
exact this (mem_span_support f)