map_comp_div' — Mathlib

English

Let G,H be DivisionInvMonoids and F a MulHomClass. If f: F and hf : ∀ a, f a⁻¹ = (f a)⁻¹, then for all g,h : ι → G, f ∘ (g / h) = f ∘ g / f ∘ h.

Русский

Пусть G,H — дивизионные моноиды, F — множество гомоморфизмов, и f удовлетворяет hf: ∀ a, f(a⁻¹) = f(a)⁻¹. Тогда для любых 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]
theorem map_comp_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹)
    (g h : ι → G) : f ∘ (g / h) = f ∘ g / f ∘ h := by ext; simp [map_div' f hf]

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