Theorems · Theorem · ring theory

DirectSum.lmap_lof

∀ {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) [inst_5 : DecidableEq ι] (i : ι) (x : M i),
  (DirectSum.lmap f) ((DirectSum.lof R ι M i) x) = (DirectSum.lof R ι N i) ((f i) x)

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEq