English
The presented module is the quotient of the free A-module on generators G by the submodule generated by the relations given by relations.relation.
Русский
Представляемый модуль является фактор-модулем свободного A-модуля на генераторах G по подмодулю, порождённому отношениями из relations.relation.
LaTeX
$$$\\mathrm{Quotient} = (\\mathrm{G} \\to_A A) \\/\\/ \\operatorname{span}_A(\\mathrm{range}(\\mathrm{relation})).$$$
Lean4
/-- The module that is presented by generators and relations given by `relations : Relations A`.
This is the quotient of the free `A`-module on `relations.G` by the submodule generated by
the given relations. -/
def Quotient :=
(relations.G →₀ A) ⧸ Submodule.span A (Set.range relations.relation)
