auxEquiv_comm — Mathlib

English

The auxiliary equivalence commutes with graded commutativity: auxEquiv(comm x) equals gradedComm(auxEquiv x).

Русский

auxEquiv сохраняет градуированную коммутативность: auxEquiv(comm x) = gradedComm(auxEquiv x).

LaTeX

$$$\mathrm{auxEquiv}_R(ℬ,𝒜)(\mathrm{comm}_{𝒜,ℬ}(x)) = \mathrm{gradedComm}_R(𝒜·,ℬ·)(\mathrm{auxEquiv}_R(𝒜,ℬ)(x))$$$

Lean4

theorem auxEquiv_comm (x : 𝒜 ᵍ⊗[R] ℬ) : auxEquiv R ℬ 𝒜 (comm 𝒜 ℬ x) = gradedComm R (𝒜 ·) (ℬ ·) (auxEquiv R 𝒜 ℬ x) :=
  LinearEquiv.eq_symm_apply _ |>.mp rfl

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