ker_π — Mathlib

English

The kernel of the map π is exactly the submodule generated by the relations of the presentation.

Русский

Ядро отображения π равно подмодулю, порождаемому отношениями презентации.

LaTeX

$$$$ \\ker(\\mathrm{solution}.\\pi) = \\operatorname{span}_A(\\mathrm{range}(\\mathrm{relations}.\\mathrm{relation})) $$$$

Lean4

theorem ker_π : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation) := by
  simpa only [← injective_fromQuotient_iff_ker_π_eq_span] using h.bijective.1

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