English
As above: X_s are all distinct; equality of X_s and X_t forces s = t.
Русский
Как выше: X_s различны; равенство X_s и X_t требует s = t.
LaTeX
$$$X_s = X_t \\iff s = t$$$
Lean4
/-- The map between multivariate formal power series induced by a map on the coefficients. -/
def map : MvPowerSeries σ R →+* MvPowerSeries σ S
where
toFun φ n := f <| coeff n φ
map_zero' := ext fun _n => f.map_zero
map_one' :=
ext fun n =>
show f (coeff n 1) = coeff n 1 by
classical
rw [coeff_one, coeff_one]
split_ifs with h
· simp only [map_one]
· simp only [map_zero]
map_add' φ ψ := ext fun n => show f (coeff n (φ + ψ)) = f (coeff n φ) + f (coeff n ψ) by simp
map_mul' φ
ψ :=
ext fun n =>
show f _ = _ by
classical
rw [coeff_mul, map_sum, coeff_mul]
apply Finset.sum_congr rfl
rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl
