auxEquiv_symm_one

Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

URI: https://scilib.ai/kg/mathlib#GradedTensorProduct.auxEquiv_symm_one

English

The inverse of the auxiliary equivalence also sends 1 to 1: (auxEquiv R 𝒜 ℬ)⁻¹ 1 = 1.

Русский

Обратное к auxEquiv отображение также посылает единицу в единицу: (auxEquiv R 𝒜 ℬ)⁻¹ 1 = 1.

LaTeX

$$$ (\mathrm{auxEquiv}_R(𝒜,ℬ))^{-1}(1) = 1 $$$

Lean4

theorem auxEquiv_symm_one : (auxEquiv R 𝒜 ℬ).symm 1 = 1 :=
  (LinearEquiv.symm_apply_eq _).mpr (auxEquiv_one _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru