From a28012c8427642abd900b51c1e6a17c888463064 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 22 Apr 2021 14:56:29 +0000 Subject: [PATCH] feat(algebra/monoid_algebra): add mem.span_support (#7323) A (very) easy lemma about `monoid_algebra`. --- src/algebra/monoid_algebra.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 1e27f851e5815..6ab5066b56a31 100644 --- a/src/algebra/monoid_algebra.lean +++ b/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 /-!