isUnit_of_isUnit_leadingCoeff_AddUnitOrder

English

If the leading coefficient of x is a unit and the order is an additive unit, then x is a unit.

Русский

Если ведущий коэффициент x является единицей и порядок является дополнительно единицей, то x является единицей.

LaTeX

$$IsUnit x.leadingCoeff → IsAddUnit x.order → IsUnit x$$

Lean4

theorem isUnit_of_isUnit_leadingCoeff_AddUnitOrder {x : HahnSeries Γ R} (hx : IsUnit x.leadingCoeff)
    (hxo : IsAddUnit x.order) : IsUnit x := by
  let ⟨⟨u, i, ui, iu⟩, h⟩ := hx
  rw [Units.val_mk] at h
  rw [h] at iu
  have h' := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ hxo.addUnit.neg_add)
  rw [sub_sub_cancel] at h'
  exact isUnit_of_mul_isUnit_right (isUnit_of_mul_eq_one _ _ h')

Похожие утверждения