map_div' — Mathlib

English

Let G,H be DivisionInvMonoids and f: G → H a MonoidHomClass with hf : ∀ a, f a⁻¹ = (f a)⁻¹. Then for all a,b ∈ G, f(a/b) = f(a)/f(b).

Русский

Пусть G,H — дивизионные инвариантные моноиды, f: G → H — моноидный гомоморфизм, удовлетворяющий hf: ∀ a, f(a⁻¹) = f(a)⁻¹. Тогда для всех a,b ∈ G выполняется f(a/b) = f(a)/f(b).

LaTeX

$$$$ \forall a,b \in G,\ f(a/b) = f(a)/f(b). $$$$

Lean4

@[to_additive]
theorem map_div' [DivInvMonoid G] [DivInvMonoid H] [MulHomClass F G H] (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) :
    f (a / b) = f a / f b := by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]

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