inv_comp — Mathlib

English

Let φ: N →* G and ψ: M →* N be monoid homomorphisms with G, H commutative groups. Then the inverse of the composition equals the composition of the inverses: φ⁻¹ ∘ ψ = (φ ∘ ψ)⁻¹.

Русский

Пусть φ: N →* G и ψ: M →* N — гомоморфизмы моноидов. Тогда обратная композиция равна композиции обратных: φ⁻¹ ∘ ψ = (φ ∘ ψ)⁻¹.

LaTeX

$$$ φ^{-1} \\circ ψ = (φ \\circ ψ)^{-1} $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_comp (φ : N →* G) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ)⁻¹ :=
  rfl

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