Theorems · Theorem · commutative algebra

Module.Relations.Solution.IsPresentation.directSum

∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {relations : ι → Module.Relations A}
  {M : ι → Type v} [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  {solution : (i : ι) → (relations i).Solution (M i)},
  (∀ (i : ι), (solution i).IsPresentation) → (Module.Relations.Solution.directSum solution).IsPresentation

Defined in

Mathlib.Algebra.Module.Presentation.DirectSum

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingDecidableEqAddCommGroupModule