finsuppToCoinvariants_single_mk — Mathlib

English

The subtype action on the coinvariants of a tensor product is trivial; i.e., the subtype action is the identity in the coinvariants.

Русский

Действие подтипов на когонвариантах тензорного произведения тривиально; иначе говоря, подтиповое действие является тождественным на когонвариантах.

LaTeX

$$IsTrivial ((toCoinvariants ρ S).comp S.subtype)$$

Lean4

@[simp]
theorem finsuppToCoinvariants_single_mk (a : α) (x : V) :
    finsuppToCoinvariants ρ α (single a <| Coinvariants.mk _ x) = Coinvariants.mk _ (single a x) := by
  simp [finsuppToCoinvariants]

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