Documentation

Ado.ForMathlib.DirectSum

source
@[simp]
theorem DirectSum.lmap_add {R : Type u_1} [Semiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f g : (i : ι) → M i →ₗ[R] N i) :
lmap (f + g) = lmap f + lmap g
source
@[simp]
theorem DirectSum.lmap_fun_add {R : Type u_1} [Semiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (f g : (i : ι) → M i →ₗ[R] N i) :
(lmap fun (i : ι) => f i + g i) = lmap f + lmap g

Eta-expanded form of DirectSum.lmap_add

source
@[simp]
theorem DirectSum.lmap_smul {R : Type u_1} [CommSemiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (c : R) (f : (i : ι) → M i →ₗ[R] N i) :
lmap (c • f) = c • lmap f
source
@[simp]
theorem DirectSum.lmap_fun_smul {R : Type u_1} [CommSemiring R] {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : ι → Type u_4} [(i : ι) → AddCommMonoid (N i)] [(i : ι) → Module R (N i)] (c : R) (f : (i : ι) → M i →ₗ[R] N i) :
(lmap fun (i : ι) => c • f i) = c • lmap f

Eta-expanded form of DirectSum.lmap_smul