surjective_π — Mathlib

English

The canonical map π from the generators to M is surjective; i.e., every element of M is reached by some linear combination of generators.

Русский

Каноническое отображение π от порождающих к M сюръективно: каждый элемент M достигается линейной комбинацией порождающих.

LaTeX

$$$$ \\operatorname{Im}(\\mathrm{solution}.\\pi) = M $$$$

Lean4

theorem surjective_π : Function.Surjective solution.π := by
  simpa only [← surjective_fromQuotient_iff_surjective_π] using h.bijective.2

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