π — Mathlib · SciLib

English

For a solution, the range of the linear map π equals the submodule of M generated by the images of all generators g under solution.var.

Русский

Для решения образ линейного отображения π равен подмодулю M, порождённому изображениями всех генераторов g через solution.var.

LaTeX

$$$\operatorname{range}(\text{solution.π}) = \operatorname{span}_A(\mathrm{Set.range}(\text{solution.var}))$$$

Lean4

/-- Given `relations : Relations A` and a solution in `relations.Solution M`, this is
the linear map `(relations.G →₀ A) →ₗ[A] M` canonically associated to the solution. -/
noncomputable def π : (relations.G →₀ A) →ₗ[A] M :=
  Finsupp.linearCombination _ solution.var

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