solutionFinsupp_isPresentation — Mathlib

English

The free module corresponds to the presentation given by finsupp-based universal construction.

Русский

Свободный модуль соответствует презентации, заданной универсальной конструкцией на основе finsupp.

LaTeX

$$$Module.Free\\, A\\ M \\equiv (Solution.IsPresentation) \\Rightarrow \\text{free}$$$

Lean4

theorem solutionFinsupp_isPresentation : relations.solutionFinsupp.IsPresentation :=
  (solutionFinsupp.isPresentationCore relations).isPresentation

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