map_comp_mul_inv — Mathlib

English

Let G,H be DivisionInvMonoids and F a MonoidHomClass. For any g,h : ι → G, f ∘ (g * h⁻¹) = (f ∘ g) * (f ∘ h)⁻¹.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem map_comp_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G) :
    f ∘ (g * h⁻¹) = f ∘ g * (f ∘ h)⁻¹ := by simp

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