presentation — Mathlib

English

The standard presentation of the R-module ⋀[R]^n M is given by the construction isPresentation, i.e., the module with generators G = ι → M modulo the relations R

Русский

Стандартная презентация R-модуля ⋀[R]^n M задаётся через конструирование isPresentation: модуль с генераторами G = ι → M по отношениям R.

LaTeX

$$$\\text{presentation } R (⋀[R]^n M) = \\mathrm{Module.Presentation}(R, ⋀[R]^n M)$.$$

Lean4

/-- The standard presentation of the `R`-module `⋀[R]^n M`. -/
@[simps! G R relation var]
noncomputable def presentation : Module.Presentation R (⋀[R]^n M) :=
  .ofIsPresentation (presentation.isPresentationCore R n M).isPresentation

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