auxEquiv_mul — Mathlib

English

The auxiliary equivalence commutes with multiplication: auxEquiv( x*y ) = gradedMul( auxEquiv(x), auxEquiv(y) ).

Русский

Вспомогательное эквивалентное отображение совместимо с умножением: auxEquiv(x*y) = gradedMul(auxEquiv(x), auxEquiv(y)).

LaTeX

$$$\operatorname{auxEquiv}_R(𝒜,ℬ)(x*y) = \operatorname{gradedMul}_R(𝒜·)(ℬ·)(\operatorname{auxEquiv}_R(𝒜,ℬ)(x), \operatorname{auxEquiv}_R(𝒜,ℬ)(y))$$$

Lean4

theorem auxEquiv_mul (x y : 𝒜 ᵍ⊗[R] ℬ) :
    auxEquiv R 𝒜 ℬ (x * y) = gradedMul R (𝒜 ·) (ℬ ·) (auxEquiv R 𝒜 ℬ x) (auxEquiv R 𝒜 ℬ y) :=
  LinearEquiv.eq_symm_apply _ |>.mp rfl

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