inv_μᵣ

Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.RightLinear.inv_μᵣ

English

Equality of inverses: inv(μᵣ F d c) = δᵣ F d c.

Русский

Сопоставление обратного: inv(μᵣ F d c) = δᵣ F d c.

LaTeX

$$$\mathrm{inv}(\mu^{\mathrm{r}} F d c) = \delta^{\mathrm{r}} F d c$$$

Lean4

@[simp]
theorem inv_μᵣ : CategoryTheory.inv (μᵣ F d c) = δᵣ F d c :=
  Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| μᵣ_comp_δᵣ F d c

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru