single_add_erase — Mathlib

English

The decomposition: single a (algebraMap k A b) equals algebraMap k (SkewMonoidAlgebra k G) b times of k G a.

Русский

Разложение: single a (algebraMap k A b) равно algebraMap k (SkewMonoidAlgebra k G) b умноженному на of k G a.

LaTeX

$$$ single\ a (algebraMap k A b) = algebraMap k (SkewMonoidAlgebra k G) b \cdot of k G a $$$

Lean4

theorem single_add_erase (a : α) (f : SkewMonoidAlgebra M α) : single a (f.coeff a) + f.erase a = f :=
  by
  apply toFinsupp_injective
  rw [single, ← toFinsupp_apply, toFinsupp_add, erase_apply_toFinsupp, Finsupp.single_add_erase]

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