English
Let R and R' be commutative rings and φ: R →+* R' a ring homomorphism. For v,w : Fin n → R, the Vandermonde projection of (φ(v i)) and (φ(w i)) equals the image of the Vandermonde projection under φ, i.e., the entries are obtained by applying φ entrywise.
Русский
Пусть R, R' — коммутативные кольца и φ: R →+* R' гомоморфизм колец. Для v, w : Fin n → R, Vandermonde-проекция от (φ(v i)) и (φ(w i)) равна образу Vandermonde-проекции от (v,w) под φ; то есть элементы получаются применением φ к каждому элементу.
LaTeX
$$$ \\mathrm{projVandermonde}(\\lambda i. \\phi(v i))(\\lambda i. \\phi(w i)) = \\phi.mapMatrix( \\mathrm{projVandermonde} v w).$$$
Lean4
theorem projVandermonde_map {R' : Type*} [CommRing R'] (φ : R →+* R') (v w : Fin n → R) :
projVandermonde (fun i ↦ φ (v i)) (fun i ↦ φ (w i)) = φ.mapMatrix (projVandermonde v w) :=
by
ext i j
simp [projVandermonde_apply]
