English
The power-series ring k[[X]] carries a normalization monoid structure, where every element f has a defined normUnit given by dividing by X^order(f).
Русский
Кольцо степенных рядов k[[X]] оснащено нормализационным моноидом: для каждого элемента f существует нормализующая единица normUnit(f), связанная с order(f).
LaTeX
$$PowerSeries k has a normalization monoid structure with normUnit(f) := (Unit_of_divided_by_X_pow_order f)^{-1}.$$
Lean4
instance : NormalizationMonoid k⟦X⟧
where
normUnit f := (Unit_of_divided_by_X_pow_order f)⁻¹
normUnit_zero := by simp only [Unit_of_divided_by_X_pow_order_zero, inv_one]
normUnit_mul := fun hf hg ↦ by
simp only [← mul_inv, inv_inj]
simp only [Unit_of_divided_by_X_pow_order_nonzero (mul_ne_zero hf hg), Unit_of_divided_by_X_pow_order_nonzero hf,
Unit_of_divided_by_X_pow_order_nonzero hg, Units.ext_iff, Units.val_mul, divXPowOrder_mul_divXPowOrder]
normUnit_coe_units := by
intro u
set u₀ := u.1 with hu
have h₀ : IsUnit u₀ := ⟨u, hu.symm⟩
rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]
exact ((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm
