Theorems · Theorem · ring theory

MonoidAlgebra.support_mul_single

Deprecated since 2026-06-18Use MonoidAlgebra.support_coeff_mul_single instead.

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

Alias of MonoidAlgebra.support_coeff_mul_single.

Defined in

Mathlib.Algebra.MonoidAlgebra.Support

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringMulIsRightCancelMul