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]