Theorems · Theorem · ring theory

MonoidAlgebra.support_coeff_single_mul

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

Defined in

Mathlib.Algebra.MonoidAlgebra.Support

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringMulIsLeftCancelMul