English
If f is a local ring hom, then the induced map between multivariate power series is a local hom: IsLocalHom (MvPowerSeries.map (σ := σ) f).
Русский
Если f — локальный кольцевой гомоморфизм, то полученный отображение между многомерными формальными степенными рядами является локальным отображением: IsLocalHom (MvPowerSeries.map (σ := σ) f).
LaTeX
$$$\text{IsLocalHom}(\mathrm{MvPowerSeries.map}(\sigma := \sigma) f)$$$
Lean4
/-- Auxiliary definition that unifies
the totalised inverse formal power series `(_)⁻¹` and
the inverse formal power series that depends on
an inverse of the constant coefficient `invOfUnit`. -/
protected noncomputable def aux (a : R) (φ : MvPowerSeries σ R) : MvPowerSeries σ R
| n =>
letI := Classical.decEq σ
if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if _ : x.2 < n then coeff x.1 φ * inv.aux a φ x.2 else 0
termination_by n => n
