star_div₀ — Mathlib

English

If R is a commutative group with zero and star, then star(x / y) = star(x) / star(y).

Русский

Если R — коммутативная группа с нулём и звёздой, то star(x / y) = star(x) / star(y).

LaTeX

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

Lean4

/-- When multiplication is commutative, `star` preserves division. -/
@[simp]
theorem star_div₀ [CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = star x / star y :=
  by
  apply op_injective
  rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]

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