toCoinvariants_mk — Mathlib

English

If g ∈ G and x ∈ V, then the action of g on the class of x in the coinvariants equals the class of ρ(g)x.

Русский

Пусть g ∈ G и x ∈ V. Тогда действие g на класс x в когонвариантах равно классy ρ(g)x.

LaTeX

$$toCoinvariants ρ S g (Coinvariants.mk _ x) = Coinvariants.mk _ (ρ g x)$$

Lean4

@[simp]
theorem toCoinvariants_mk (g : G) (x : V) : toCoinvariants ρ S g (Coinvariants.mk _ x) = Coinvariants.mk _ (ρ g x) :=
  rfl

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