Theorems · Theorem · ring theory

SkewMonoidAlgebra.coeff_update_apply

Deprecated since 2026-07-04Use Finsupp.update_apply instead.

∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a a' : α) (b : M)
  [inst_1 : DecidableEq α], (f.update a b).coeff a' = if a' = a then b else f.coeff a'

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Single

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEq