Theorems · Theorem · ring theory

DirectSum.toAddMonoidHom_lmap

∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  (DirectSum.lmap f).toAddMonoidHom = DirectSum.map fun i => (f 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

SemiringAddCommMonoidModuleAddCommMonoidModule