decompose_symm_mul — Mathlib

English

The symmetric/decomposed inverse respects multiplication: (decompose 𝒜).symm (x y) = (decompose 𝒜).symm x · (decompose 𝒜).symm y.

Русский

Обратное разложения по симметрии сохраняет умножение: (decompose 𝒜).symm (xy) = (decompose 𝒜).symm x · (decompose 𝒜).symm y.

LaTeX

$$$ (\mathrm{decompose} 𝒜)^{-1} (xy) = (\mathrm{decompose} 𝒜)^{-1} x \cdot (\mathrm{decompose} 𝒜)^{-1} y. $$$

Lean4

@[simp]
theorem decompose_symm_mul (x y : ⨁ i, 𝒜 i) :
    (decompose 𝒜).symm (x * y) = (decompose 𝒜).symm x * (decompose 𝒜).symm y :=
  map_mul (decomposeRingEquiv 𝒜).symm x y

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