∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {R' : Type u_3} [inst_1 : CommRing R'] (φ : R →+* R') (v w : Fin n → R),
  (Matrix.projVandermonde (fun i => φ (v i)) fun i => φ (w i)) = φ.mapMatrix (Matrix.projVandermonde v w)