Lemmas about the support of a finitely supported function

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

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

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

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

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

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

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

theorem MonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) : f ∈ Submodule.span k (↑(MonoidAlgebra.of k G) '' ↑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₂} [Semiring k] [DecidableEq G] [Add G] (a : AddMonoidAlgebra k G) (b : AddMonoidAlgebra k G) : (a * b).support ⊆ Finset.biUnion a.support fun a₁ => Finset.biUnion b.support fun a₂ => {a₁ + a₂}

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

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

theorem AddMonoidAlgebra.mem_span_support {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) : f ∈ Submodule.span k (↑(AddMonoidAlgebra.of k G) '' ↑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₂} [Semiring k] (f : AddMonoidAlgebra k G) : f ∈ Submodule.span k (AddMonoidAlgebra.of' k G '' ↑f.support)

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