Lemmas about the support of a finitely supported function

theorem MonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) : (a * b).support ⊆ a.support * b.support

theorem AddMonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (a b : AddMonoidAlgebra k G) : (a * b).support ⊆ a.support + b.support

theorem MonoidAlgebra.support_single_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (f : MonoidAlgebra k G) (r : k) (a : G) : (single a r * f).support ⊆ Finset.image (fun (x : G) => a * x) f.support

theorem AddMonoidAlgebra.support_single_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (f : AddMonoidAlgebra k G) (r : k) (a : G) : (single a r * f).support ⊆ Finset.image (fun (x : G) => a + x) f.support

theorem MonoidAlgebra.support_mul_single_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (f : MonoidAlgebra k G) (r : k) (a : G) : (f * single a r).support ⊆ Finset.image (fun (x : G) => x * a) f.support

theorem AddMonoidAlgebra.support_mul_single_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (f : AddMonoidAlgebra k G) (r : k) (a : G) : (f * single a r).support ⊆ Finset.image (fun (x : G) => x + a) f.support

theorem MonoidAlgebra.support_single_mul_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ (y : k), r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) : (single x r * f).support = Finset.image (fun (x_1 : G) => x * x_1) f.support

theorem AddMonoidAlgebra.support_single_mul_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (f : AddMonoidAlgebra k G) {r : k} (hr : ∀ (y : k), r * y = 0 ↔ y = 0) {x : G} (lx : IsAddLeftRegular x) : (single x r * f).support = Finset.image (fun (x_1 : G) => x + x_1) f.support

theorem MonoidAlgebra.support_mul_single_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ (y : k), y * r = 0 ↔ y = 0) {x : G} (rx : IsRightRegular x) : (f * single x r).support = Finset.image (fun (x_1 : G) => x_1 * x) f.support

theorem AddMonoidAlgebra.support_mul_single_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (f : AddMonoidAlgebra k G) {r : k} (hr : ∀ (y : k), y * r = 0 ↔ y = 0) {x : G} (rx : IsAddRightRegular x) : (f * single x r).support = Finset.image (fun (x_1 : G) => x_1 + x) f.support

theorem MonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 ↔ y = 0) (x : G) : (f * single x r).support = Finset.map (mulRightEmbedding x) f.support

theorem AddMonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [IsRightCancelAdd G] (f : AddMonoidAlgebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 ↔ y = 0) (x : G) : (f * single x r).support = Finset.map (addRightEmbedding x) f.support

theorem MonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ (y : k), r * y = 0 ↔ y = 0) (x : G) : (single x r * f).support = Finset.map (mulLeftEmbedding x) f.support

theorem AddMonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [IsLeftCancelAdd G] (f : AddMonoidAlgebra k G) (r : k) (hr : ∀ (y : k), r * y = 0 ↔ y = 0) (x : G) : (single x r * f).support = Finset.map (addLeftEmbedding x) f.support

theorem MonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [One G] : Finsupp.support 1 ⊆ 1

theorem AddMonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] : Finsupp.support 1 ⊆ 0

@[simp]

theorem MonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] [NeZero 1] : Finsupp.support 1 = 1

@[simp]

theorem AddMonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] [NeZero 1] : Finsupp.support 1 = 0

theorem MonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) : f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

An element of k[G] is in the subalgebra generated by its support.

theorem AddMonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) : f ∈ Submodule.span k (of' k G '' ↑f.support)

An element of k[G] is in the submodule generated by its support.

@[deprecated AddMonoidAlgebra.mem_span_support (since := "2025-12-08")]

theorem AddMonoidAlgebra.mem_span_support' {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) : f ∈ Submodule.span k (of' k G '' ↑f.support)

Alias of AddMonoidAlgebra.mem_span_support.

---

An element of k[G] is in the submodule generated by its support.