English
A Hahn series x is a unit iff its leading coefficient is a unit in the coefficient ring.
Русский
Серия Ханна x является единицей тогда и только тогда, когда её ведущий коэффициент является единицей в кольце коэффициентов.
LaTeX
$$IsUnit x ↔ IsUnit x.leadingCoeff$$
Lean4
theorem isUnit_iff {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit (x.leadingCoeff) :=
by
constructor
· rintro ⟨⟨u, i, ui, iu⟩, rfl⟩
refine isUnit_of_mul_eq_one (u.leadingCoeff) (i.leadingCoeff) ((coeff_mul_order_add_order u i).symm.trans ?_)
rw [ui, coeff_one, if_pos]
rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]
· rintro ⟨⟨u, i, ui, iu⟩, hx⟩
rw [Units.val_mk] at hx
rw [hx] at iu
have h := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ (neg_add_cancel x.order))
rw [sub_sub_cancel] at h
exact isUnit_of_mul_isUnit_right (isUnit_of_mul_eq_one _ _ h)
