English
If the leading coefficient is a unit and the order is an additive unit, then x is a unit; the proof uses unit_aux and one_sub_self_mul_hsum_powers.
Русский
Если ведущий коэффициент является единицей и порядок — единица, то x является единицей; доказательство использует unit_aux и one_sub_self_mul_hsum_powers.
LaTeX
$$IsUnit x.leadingCoeff → IsAddUnit x.order → IsUnit x$$
Lean4
/-- The additive valuation on `HahnSeries Γ R`, returning the smallest index at which
a Hahn Series has a nonzero coefficient, or `⊤` for the 0 series. -/
def addVal : AddValuation (HahnSeries Γ R) (WithTop Γ) :=
AddValuation.of orderTop orderTop_zero (orderTop_one) (fun _ _ => min_orderTop_le_orderTop_add) fun x y =>
by
by_cases hx : x = 0; · simp [hx]
by_cases hy : y = 0; · simp [hy]
rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy, ←
order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe, order_mul hx hy]
