ofMapDiv — Mathlib

English

Given a map f preserving division, produce a monoid homomorphism from G to H.

Русский

Дано отображение f, сохраняющее деление, строим моноид-гомоморфизм G → H.

LaTeX

$$$\operatorname{ofMapDiv}(f, hf) : G \to^* H$$$

Lean4

/-- Define a morphism of additive groups given a map which respects ratios. -/
@[to_additive /-- Define a morphism of additive groups given a map which respects difference. -/
    ]
def ofMapDiv {H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) : G →* H :=
  ofMapMulInv f (by simpa only [div_eq_mul_inv] using hf)

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