toTensorAlgebra_gOne — Mathlib

English

The canonical embedding sends the unit of the graded monoid to the unit of the tensor algebra.

Русский

Каноническое вложение отправляет единицу градуированного монадного умножения в единицу тензорной алгебры.

LaTeX

$$$ TensorPower.toTensorAlgebra (GradedMonoid.GOne.one) = 1 $$$

Lean4

@[simp]
theorem toTensorAlgebra_gOne : TensorPower.toTensorAlgebra (@GradedMonoid.GOne.one _ (fun n => ⨂[R]^n M) _ _) = 1 := by
  simp [GradedMonoid.GOne.one, TensorPower.toTensorAlgebra_tprod]

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