# Lemmas about the support of a finitely supported function #

theorem MonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [] [Mul G] [] (a : ) (b : ) :
(a * b).support a.support * b.support
theorem MonoidAlgebra.support_single_mul_subset {k : Type u₁} {G : Type u₂} [] [] [Mul G] (f : ) (r : k) (a : G) :
().support Finset.image (fun (x : G) => a * x) f.support
theorem MonoidAlgebra.support_mul_single_subset {k : Type u₁} {G : Type u₂} [] [] [Mul G] (f : ) (r : k) (a : G) :
().support Finset.image (fun (x : G) => x * a) f.support
theorem MonoidAlgebra.support_single_mul_eq_image {k : Type u₁} {G : Type u₂} [] [] [Mul G] (f : ) {r : k} (hr : ∀ (y : k), r * y = 0 y = 0) {x : G} (lx : ) :
().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₂} [] [] [Mul G] (f : ) {r : k} (hr : ∀ (y : k), y * r = 0 y = 0) {x : G} (rx : ) :
().support = Finset.image (fun (x_1 : G) => x_1 * x) f.support
theorem MonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [] [Mul G] [] (f : ) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
().support = Finset.map f.support
theorem MonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [] [Mul G] [] (f : ) (r : k) (hr : ∀ (y : k), r * y = 0 y = 0) (x : G) :
().support = Finset.map () f.support
theorem MonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [] [One G] :
@[simp]
theorem MonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [] [One G] [] :
theorem MonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [] [] (f : ) :
f Submodule.span k (() '' f.support)

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

theorem AddMonoidAlgebra.support_mul {k : Type u₁} {G : Type u₂} [] [] [Add G] (a : ) (b : ) :
(a * b).support a.support + b.support
theorem AddMonoidAlgebra.support_mul_single {k : Type u₁} {G : Type u₂} [] [Add G] [] (f : ) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
().support = Finset.map f.support
theorem AddMonoidAlgebra.support_single_mul {k : Type u₁} {G : Type u₂} [] [Add G] [] (f : ) (r : k) (hr : ∀ (y : k), r * y = 0 y = 0) (x : G) :
().support = Finset.map () f.support
theorem AddMonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [] [Zero G] :
@[simp]
theorem AddMonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [] [Zero G] [] :
theorem AddMonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [] [] (f : ) :
f Submodule.span k (() '' f.support)

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

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

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