coe_of_map_mul_inv — Mathlib

English

Construct a group homomorphism from a map that preserves right division x y^{-1} → f(x) f(y)^{-1}, via an explicit Morita-style constructor.

Русский

Построение гомоморфизма из отображения, сохраняющего правое деление, через явный конструктор.

LaTeX

$$$\operatorname{ofMapMulInv}(f, map\_div) = \operatorname{mk}' f\,\dots$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_of_map_mul_inv {H : Type*} [Group H] (f : G → H) (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) :
    ↑(ofMapMulInv f map_div) = f :=
  rfl

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