star_mul' — Mathlib

English

In a commutative ring, star distributes over multiplication: star(xy) = star x · star y.

Русский

В коммутативном кольце звезда распределяется по умножению: star(xy) = star x · star y.

LaTeX

$$$$ \star(x \cdot y) = \star x \cdot \star y. $$$$

Lean4

/-- In a commutative ring, make `simp` prefer leaving the order unchanged. -/
@[simp]
theorem star_mul' [CommMagma R] [StarMul R] (x y : R) : star (x * y) = star x * star y :=
  (star_mul x y).trans (mul_comm _ _)

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