map_comp_div — Mathlib

English

Let G be a group, H a division monoid, 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 / h) = f \circ g / f \circ h. $$$$

Lean4

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

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