Documentation

Mathlib.Algebra.MonoidAlgebra.Support

Lemmas about the support of a finitely supported function #

source
theorem MonoidAlgebra.support_coeff_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (x y : MonoidAlgebra k G) :
(x * y).coeff.support ⊆ x.coeff.support * y.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (x y : AddMonoidAlgebra k G) :
(x * y).coeff.support ⊆ x.coeff.support + y.coeff.support
source
@[deprecated MonoidAlgebra.support_coeff_mul_subset (since := "2026-06-18")]
theorem MonoidAlgebra.support_single_mul_eq_image {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (x y : MonoidAlgebra k G) :
(x * y).coeff.support ⊆ x.coeff.support * y.coeff.support

Alias of MonoidAlgebra.support_coeff_mul_subset.

source
theorem MonoidAlgebra.support_coeff_single_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (x : MonoidAlgebra k G) (r : k) (a : G) :
(single a r * x).coeff.support ⊆ Finset.image (fun (x : G) => a * x) x.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_single_mul_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (x : AddMonoidAlgebra k G) (r : k) (a : G) :
(single a r * x).coeff.support ⊆ Finset.image (fun (x : G) => a + x) x.coeff.support
source
theorem MonoidAlgebra.support_coeff_mul_single_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] [DecidableEq G] (x : MonoidAlgebra k G) (r : k) (a : G) :
(x * single a r).coeff.support ⊆ Finset.image (fun (x : G) => x * a) x.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_mul_single_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] [DecidableEq G] (x : AddMonoidAlgebra k G) (r : k) (a : G) :
(x * single a r).coeff.support ⊆ Finset.image (fun (x : G) => x + a) x.coeff.support
source
theorem MonoidAlgebra.support_coeff_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).coeff.support = Finset.image (fun (x_1 : G) => x * x_1) f.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_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).coeff.support = Finset.image (fun (x_1 : G) => x + x_1) f.coeff.support
source
theorem MonoidAlgebra.support_coeff_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).coeff.support = Finset.image (fun (x_1 : G) => x_1 * x) f.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_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).coeff.support = Finset.image (fun (x_1 : G) => x_1 + x) f.coeff.support
source
@[deprecated MonoidAlgebra.support_coeff_mul_single_eq_image (since := "2026-06-18")]
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).coeff.support = Finset.image (fun (x_1 : G) => x_1 * x) f.coeff.support

Alias of MonoidAlgebra.support_coeff_mul_single_eq_image.

source
theorem MonoidAlgebra.support_coeff_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).coeff.support = Finset.map (mulRightEmbedding x) f.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_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).coeff.support = Finset.map (addRightEmbedding x) f.coeff.support
source
@[deprecated MonoidAlgebra.support_coeff_mul_single (since := "2026-06-18")]
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).coeff.support = Finset.map (mulRightEmbedding x) f.coeff.support

Alias of MonoidAlgebra.support_coeff_mul_single.

source
theorem MonoidAlgebra.support_coeff_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).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support
source
theorem AddMonoidAlgebra.support_coeff_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).coeff.support = Finset.map (addLeftEmbedding x) f.coeff.support
source
@[deprecated MonoidAlgebra.support_coeff_single_mul (since := "2026-06-18")]
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).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support

Alias of MonoidAlgebra.support_coeff_single_mul.

source
theorem MonoidAlgebra.support_coeff_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :
(coeff 1).support ⊆ 1
source
theorem AddMonoidAlgebra.support_coeff_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :
(coeff 1).support ⊆ 0
source
@[deprecated MonoidAlgebra.support_coeff_one_subset (since := "2026-06-18")]
theorem MonoidAlgebra.support_one_subset {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :
(coeff 1).support ⊆ 1

Alias of MonoidAlgebra.support_coeff_one_subset.

source
@[simp]
theorem MonoidAlgebra.support_coeff_one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] [NeZero 1] :
(coeff 1).support = 1
source
@[simp]
theorem AddMonoidAlgebra.support_coeff_one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] [NeZero 1] :
(coeff 1).support = 0
source
@[deprecated MonoidAlgebra.support_coeff_one (since := "2026-06-18")]
theorem MonoidAlgebra.support_one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] [NeZero 1] :
(coeff 1).support = 1

Alias of MonoidAlgebra.support_coeff_one.

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

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

source
@[deprecated MonoidAlgebra.mem_span_support_coeff (since := "2026-06-18")]
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.coeff.support)

Alias of MonoidAlgebra.mem_span_support_coeff.

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

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

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

source
@[deprecated AddMonoidAlgebra.mem_span_support_coeff (since := "2026-06-18")]
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.coeff.support)

Alias of AddMonoidAlgebra.mem_span_support_coeff.

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