star_div — Mathlib

English

In a commutative group, star distributes over division: star(x / y) = star x / star y.

Русский

В коммутативной группе звездой распределяется деление: star(x / y) = star x / star y.

LaTeX

$$$$ \star\left(\dfrac{x}{y}\right) = \dfrac{\star x}{\star y}. $$$$

Lean4

/-- When multiplication is commutative, `star` preserves division. -/
@[simp]
theorem star_div [CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y :=
  map_div (starMulAut : R ≃* R) _ _

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