kroneckerTMulLinearEquiv_one — Mathlib

English

The Kronecker TMul linear equivalence sends the identity to the identity, i.e., kroneckerTMulLinearEquiv(1) = 1.

Русский

Кронекерово линейное эквивалентное отображение переводит единицу в единицу: kroneckerTMulLinearEquiv(1) = 1.

LaTeX

$$$ kroneckerTMulLinearEquiv_{l,m,n,p}(1) = 1 $$$

Lean4

@[simp]
theorem kroneckerTMulLinearEquiv_one [Module S A] [IsScalarTower R S A] :
    kroneckerTMulLinearEquiv m m n n R S A B 1 = 1 := by simp [Algebra.TensorProduct.one_def]

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