auxEquiv_one — Mathlib

English

The auxiliary equivalence preserves the unit: auxEquiv R 𝒜 ℬ 1 = 1.

Русский

Вспомогательное эквивалентное отображение сохраняет единицу: auxEquiv R 𝒜 ℬ 1 = 1.

LaTeX

$$$\operatorname{auxEquiv}_R(𝒜,ℬ)(1) = 1$$$

Lean4

theorem auxEquiv_one : auxEquiv R 𝒜 ℬ 1 = 1 := by
  rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one, DirectSum.decompose_one,
    Algebra.TensorProduct.one_def]

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