[Merged by Bors] - feat(algebra/monoid_algebra): add mem.span_support

src/algebra/monoid_algebra.lean

@@ -601,6 +601,17 @@ calc (f * g) x = sum g (λ a b, (f * single a b) x) :
 
 end
 
+section span
+
+variables [semiring k] [mul_one_class G]
+
+lemma mem_span_support (f : monoid_algebra k G) :
+  f ∈ submodule.span k (monoid_algebra.of k G '' (f.support : set G)) :=
+by rw [monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single,
+  finsupp.mem_supported]
+
+end span
+
 end monoid_algebra
 
 /-! ### Additive monoids -/
@@ -890,6 +901,17 @@ lemma lift_nc_smul {R : Type*} [add_zero_class G] [semiring R] (f : k →+* R)
 
 end misc_theorems
 
+section span
+
+variables [semiring k] [add_zero_class G]
+
+lemma mem_span_support (f : add_monoid_algebra k G) :
+  f ∈ submodule.span k (add_monoid_algebra.of k G '' (f.support : set G)) :=
+by rw [add_monoid_algebra.of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single,
+  finsupp.mem_supported]
+
+end span
+
 end add_monoid_algebra
 
 /-!