free — Mathlib

English

The direct sum inherits a presentation by generators and relations from the per-index presentations.

Русский

Прямая сумма наследует презентацию, заданную генераторами и отношениями из презентаций по индексам.

LaTeX

$$$(Module.Presentation.directSum pres).IsPresentation$$$

Lean4

theorem free {solution : relations.Solution M} (h : solution.IsPresentation) : Module.Free A M :=
  Free.of_equiv ((solutionFinsupp_isPresentation relations).uniq h)

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