ofIsPresentation — Mathlib

English

From a presentation data, one obtains a canonical presentation of the same module M.

Русский

По данным презентации получается каноническая презентация того же модуля M.

LaTeX

$$$\\text{ofIsPresentation}(h):\\ \\text{Presentation}_{A,M}$ where $h$ is a presentation of $M$.$$

Lean4

/-- Constructor for `Module.Presentation`. -/
@[simps toRelations toSolution]
def ofIsPresentation {relations : Relations.{w₀, w₁} A} {solution : relations.Solution M}
    (h : solution.IsPresentation) : Presentation.{w₀, w₁} A M
    where
  __ := relations
  toSolution := solution
  toIsPresentation := h

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