Theorems · Theorem · ring theory

DirectSum.coe_congrAddEquiv

∀ {ι : Type u_2} {N : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (N i)] {P : ι → Type u_4}
  [inst_1 : (i : ι) → AddCommMonoid (P i)] (u : (i : ι) → N i ≃+ P i),
  ⇑(DirectSum.congrAddEquiv u).toAddMonoidHom = ⇑(DirectSum.map fun i => (u i).toAddMonoidHom)

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid