coinvariantsTprodLeftRegularLEquiv_apply

English

The abbreviation toCoinvariantsKer is the G-representation structure on the kernel of ρ restricted to S.

Русский

Аббревиатура toCoinvariantsKer задаёт структуру G-представления на ядре ρ|_S.

LaTeX

$$toCoinvariantsKer : Representation k G (ker (ρ.comp S.subtype))$$

Lean4

@[simp]
theorem coinvariantsTprodLeftRegularLEquiv_apply (x : (ρ.tprod (leftRegular k G)).Coinvariants) :
    coinvariantsTprodLeftRegularLEquiv ρ x = ofCoinvariantsTprodLeftRegular ρ x := by rfl

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