Theorems · Inductive type · commutative algebra

Module.Relations.Solution.IsPresentation

{A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → relations.Solution M → Prop

Given relations : Relations A, an A-module M and solution : relations.Solution M, this property asserts that solution gives a presentation of M by generators and relations.

Defined in

Mathlib.Algebra.Module.Presentation.Basic

Cited by

39 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

RingAddCommGroupModule