algHom_surjective — Mathlib

English

The canonical algebra homomorphism from the tensor algebra to the symmetric algebra is surjective.

Русский

Канонический алгебра-гомоморфизм от тензорной алгебры к симметрической алгебре сюръективен.

LaTeX

$$$\text{algHom}_R^M : \mathrm{TensorAlgebra}(R,M) \twoheadrightarrow \mathrm{SymmetricAlgebra}(R,M)$ is surjective.$$

Lean4

theorem algHom_surjective : Function.Surjective (algHom R M) :=
  RingQuot.mkAlgHom_surjective _ _

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