toQuotient — Mathlib

English

There is a canonical surjective linear map from the free A-module on G to the quotient, denoted toQuotient.

Русский

Существует каноническое сюръективное линейное отображение от свободного A-модуля на G к фактору, обозначаемое as toQuotient.

LaTeX

$$$\\text{toQuotient} : (\\mathrm{G} \\to_A A) \\to_A \\mathrm{relations.Quotient}.$$$

Lean4

/-- The canonical (surjective) linear map `(relations.G →₀ A) →ₗ[A] relations.Quotient`. -/
noncomputable def toQuotient : (relations.G →₀ A) →ₗ[A] relations.Quotient :=
  Submodule.mkQ _

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