actionUnitIso_inv_naturality — Mathlib

English

A symmetric form of the naturality of the unit isomorphism for the right action.

Русский

Симметричная форма натуральности изоморфизма единицы для правого действия.

LaTeX

$$actionUnitIso_inv_naturality'$$

Lean4

@[reassoc]
theorem actionUnitIso_inv_naturality {d d' : D} (f : d ⟶ d') : (ρᵣ d).inv ≫ f ⊵ᵣ (𝟙_ C) = f ≫ (ρᵣ d').inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

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