English
Given x, r, oinv, and conditions, the expression 0 < (1 - single oinv r * x).orderTop holds, establishing a key nontrivial positive order.
Русский
Заданo x, r и другие условия; тогда 0 < (1 - single oinv r * x).orderTop, что дает важное положительное значение порядка.
LaTeX
$$0 < (1 - single oinv r * x).orderTop$$
Lean4
theorem unit_aux (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1) (oinv : Γ) (hxo : oinv + x.order = 0) :
0 < (1 - single oinv r * x).orderTop :=
by
let y := (x - single x.order x.leadingCoeff)
by_cases hy : y = 0
· have hrx : (single oinv) r * x = 1 := by rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]
· have hr' : IsRegular r := IsUnit.isRegular <| isUnit_of_mul_eq_one r x.leadingCoeff hr
have hy' : 0 < (single oinv r * y).order :=
by
rw [(order_single_mul_of_isRegular hr' hy)]
refine pos_of_lt_add_right (a := x.order) ?_
rw [← add_assoc, add_comm x.order, hxo, zero_add]
exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm _ hxo, orderTop_neg]
exact zero_lt_orderTop_of_order hy'
