Theorems · Theorem · ring theory

MonoidAlgebra.mem_span_support_coeff

∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : MulOneClass G] (f : MonoidAlgebra k G),
  f ∈ Submodule.span k (⇑(MonoidAlgebra.of k G) '' ↑f.coeff.support)

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

Defined in

Mathlib.Algebra.MonoidAlgebra.Support

Cited by

2 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringMulOneClass