rightUnitor_inv_tensor_one_mul — Mathlib

English

For any morphism f: X → M, the inverse right unitor interacts with η to yield f: (ρ_M)^{-1} ∘ (f ⊗ η) ∘ μ = f.

Русский

Для любого отображения f: X → M обратный правый унитор взаимодействует с η так, что получается f: (ρ_M)^{-1} ∘ (f ⊗ η) ∘ μ = f.

LaTeX

$$$ (\rho_M)^{-1} \circ (f \otimes \eta) \circ \mu = f $$$

Lean4

@[reassoc (attr := mon_tauto)]
theorem rightUnitor_inv_tensor_one_mul (f : X₁ ⟶ M) : (ρ_ _).inv ≫ (f ⊗ₘ η) ≫ μ = f := by simp [tensorHom_def]

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