isPresentation_mk — Mathlib

English

If h1 and h2 hold, giving a presentation via submodule span and kernel equality, then the given solution is a presentation.

Русский

Если выполнены условия h1 и h2, задающие презентaцию через порожденный подмодуль и равенство ядра, то данное решение является презентацией.

LaTeX

$$$(h_1 : \\operatorname{span}_A(\\operatorname{range} solution.var)=\\top) \\rightarrow (h_2 : \\ker solution.\\π = \\operatorname{span}_A(\\operatorname{range} relations.relation)) \\Rightarrow solution.IsPresentation$$$

Lean4

theorem isPresentation_mk (h₁ : Submodule.span A (Set.range solution.var) = ⊤)
    (h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)) : solution.IsPresentation := by
  rw [isPresentation_iff]; constructor <;> assumption

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