Theorems · Theorem · group theory

List.vadd_sum

∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddZeroClass N] [inst_2 : AddAction M N]
  [VAddAssocClass M N N] [VAddCommClass M N N] (l : List N) (m : M),
  l.length • m +ᵥ l.sum = (List.map (fun x => m +ᵥ x) l).sum

Defined in

Mathlib.Algebra.BigOperators.GroupWithZero.Action

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

AddMonoidAddZeroClassAddActionVAddAssocClassVAddCommClass