update

Mathlib.Algebra.SkewMonoidAlgebra.Single

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.update

Lean4

/-- Replace the coefficent of an element `f` of a skew monoid algebra at a given point `a : α` by
a given value `b : M`.
If `b = 0`, this amounts to removing `a` from the support of `f`.
Otherwise, if `a` was not in the `support` of `f`, it is added to it. -/
@[simps]
def update : SkewMonoidAlgebra M α :=
  ⟨f.toFinsupp.update a b⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru