coinvariantsToFinsupp_mk_single — Mathlib

English

For any α, the image of the basis element corresponding to a under coinvariantsToFinsupp is the corresponding singleton in α-indexed coinvariants.

Русский

Для любого α образ базисного элемента, соответствующего a, под действием coinvariantsToFinsupp переходит в соответствующий сингл в когонвариантах, индексируемых α.

LaTeX

$$coinvariantsToFinsupp_mk_single (x) (a) : coinvariantsToFinsupp ρ α (Coinvariants.mk _ (single x a)) = single x (Coinvariants.mk _ a)$$

Lean4

@[simp]
theorem coinvariantsToFinsupp_mk_single (x : α) (a : V) :
    coinvariantsToFinsupp ρ α (Coinvariants.mk _ (single x a)) = single x (Coinvariants.mk _ a) := by
  simp [coinvariantsToFinsupp]

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