endRingEquiv_comp_ρ — Mathlib

English

The same compatibility as above holds with the forward end ring isomorphism: composing its direct map with ρ yields ρ.

Русский

Та же совместимость: композиция прямого отображения энд-кольца с ρ даёт ρ.

LaTeX

$$(MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj)).comp (Action.ρ V) = ρ V$$

Lean4

@[simp]
theorem endRingEquiv_comp_ρ (V : FDRep R G) :
    (MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj)).comp (Action.ρ V) = ρ V :=
  rfl

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