map_div — Mathlib

English

A multiplicative equivalence of groups preserves division: for all x,y in G, h(x/y) = h(x)/h(y).

Русский

Мультипликативная эквивалентность групп сохраняет деление: для любых x,y в G верно h(x/y) = h(x)/h(y).

LaTeX

$$$\forall x,y\in G:\ h(x/y) = h(x)/h(y)$$$

Lean4

/-- A multiplicative equivalence of groups preserves division. -/
@[to_additive /-- An additive equivalence of additive groups preserves subtractions. -/
    ]
protected theorem map_div [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) : h (x / y) = h x / h y :=
  map_div h x y

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