prodMonoidal_rightUnitor_inv_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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