Theorems · Theorem · ring theory

MonoidAlgebra.support_coeff_single_mul_eq_image

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

Defined in

Mathlib.Algebra.MonoidAlgebra.Support

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringMulDecidableEq