A multivariable power series has a prescribed linear term when its difference from the corresponding linear form has total order at least two.
The multivariable linear form sum_i L_i X_i.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
namespace SameUniformizer
variable {R : Type*} [CommRing R]
variable {σ : Type*} [Fintype σ]def linearForm (L : σ → R) : MvPowerSeries σ RStates the theorem constantCoeff_linearForm.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
namespace SameUniformizer
variable {R : Type*} [CommRing R]
variable {σ : Type*} [Fintype σ]theorem constantCoeff_linearForm (L : σ → R) :
MvPowerSeries.constantCoeff (linearForm L) = 0A series has prescribed linear term L when its difference from sum_i L_i X_i has total order at least two.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
namespace SameUniformizer
variable {R : Type*} [CommRing R]
variable {σ : Type*} [Fintype σ]def HasLinearTerm (H : MvPowerSeries σ R) (L : σ → R) : PropA series with a prescribed linear term has zero constant coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
namespace SameUniformizer
variable {R : Type*} [CommRing R]
variable {σ : Type*} [Fintype σ]
namespace HasLinearTerm
variable {H : MvPowerSeries σ R} {L : σ → R}theorem constantCoeff_eq_zero (h : HasLinearTerm H L) :
MvPowerSeries.constantCoeff H = 0Consequently the series can genuinely be substituted into a one-variable power series.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LubinTate
namespace SameUniformizer
variable {R : Type*} [CommRing R]
variable {σ : Type*} [Fintype σ]
namespace HasLinearTerm
variable {H : MvPowerSeries σ R} {L : σ → R}theorem hasSubst (h : HasLinearTerm H L) :
PowerSeries.HasSubst H