map_comp_inv — Mathlib

English

Let G be a group, H a division monoid, and f a monoid homomorphism. For any g : ι → G, f ∘ g⁻¹ = (f ∘ g)⁻¹.

Русский

Пусть G — группа, H — дивизионный моноид, f — моноидный гомоморфизм. Для любого g : ι → G имеет место f ∘ g⁻¹ = (f ∘ g)⁻¹.

LaTeX

$$$$ \forall g: \iota \to G,\ f \circ g^{-1} = (f \circ g)^{-1}. $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) : f ∘ g⁻¹ = (f ∘ g)⁻¹ := by
  ext; simp

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