Theorems · Theorem · group theory

DirectSum.map_comp

∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) {γ : ι → Type u_6}
  [inst_2 : (i : ι) → AddCommMonoid (γ i)] (g : (i : ι) → β i →+ γ i),
  (DirectSum.map fun i => (g i).comp (f i)) = (DirectSum.map g).comp (DirectSum.map f)

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidAddCommMonoid