inv_actionHom — Mathlib

English

If f and g are isomorphisms, then inv (f ⊙ₗₘ g) equals inv f ⊙ₗₘ inv g.

Русский

Если f и g — изоморфизмы, то inv (f ⊙ₗₘ g) = inv f ⊙ₗₘ inv g.

LaTeX

$$$inv (f ⊙_\ell\_m g) = inv(f) ⊙_\ell\_m inv(g)$$$

Lean4

@[simp]
theorem inv_actionHom {x y : C} {x' y' : D} (f : x ⟶ y) (g : x' ⟶ y') [IsIso f] [IsIso g] :
    inv (f ⊙ₗₘ g) = (inv f) ⊙ₗₘ (inv g) :=
  IsIso.inv_eq_of_hom_inv_id <| by simp [← actionHom_comp]

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