∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (i : ι), (LinearMap.proj i).toAddMonoidHom = Pi.evalAddMonoidHom φ i