prodMonoidal_rightUnitor_inv_fst — Mathlib

English

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

Русский

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

LaTeX

$$$((\\rho_X).inv)_{1} = (\\rho_{X_1}).inv$$$

Lean4

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

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