prodMonoidal_rightUnitor_hom_snd — Mathlib

English

For X = (X1, X2) the second component of the right unitor at X equals the right unitor of X2.

Русский

Для X = (X1, X2) правая униторная композиция в X по второй компоненте равна правому унитору X2.

LaTeX

$$$((\\rho_X).hom)_{2} = (\\rho_{X_2}).hom$$$

Lean4

@[simp]
theorem prodMonoidal_rightUnitor_hom_snd (X : C₁ × C₂) : ((ρ_ X).hom : X ⊗ 𝟙_ _ ⟶ X).2 = (ρ_ X.2).hom :=
  by
  cases X
  rfl

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