Theorems · Theorem · commutative algebra

Module.Presentation.directSum_var

∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)) (i : ι) (g : (pres i).G),
  (Module.Presentation.directSum pres).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((pres i).var g)

Defined in

Mathlib.Algebra.Module.Presentation.DirectSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingDecidableEqAddCommGroupModule