toExterior_ι — Mathlib

English

The exterior algebra map sends the tensor algebra injection ι_R m to the exterior algebra injection ι_R m; i.e., ι is preserved by the passage from tensor to exterior algebra.

Русский

ОтображениеExterior переводит вложение тензорной алгебры ι_R m в вложение exterior алгебры ι_R m; то есть вложение сохраняется при переходе от тензорной алгебры к exterior.

LaTeX

$$$ \\text{TensorAlgebra.toExterior} (\\text{TensorAlgebra.}\\iota_R m) = \\text{ExteriorAlgebra}.\\iota_R m $$$

Lean4

@[simp]
theorem toExterior_ι (m : M) : TensorAlgebra.toExterior (TensorAlgebra.ι R m) = ExteriorAlgebra.ι R m := by
  simp [toExterior]

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