decompose_mul — Mathlib

English

Decomposition preserves multiplication: the decomposition of a product equals the product of decompositions.

Русский

Разложение сохраняет умножение: разложение произведения равно произведению разложений.

LaTeX

$$$\ decompose 𝒜 (xy) = decompose 𝒜 x \cdot decompose 𝒜 y.$$$

Lean4

@[simp]
theorem decompose_mul (x y : A) : decompose 𝒜 (x * y) = decompose 𝒜 x * decompose 𝒜 y :=
  map_mul (decomposeRingEquiv 𝒜) x y

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