eq_divided_by_X_pow_order_Iff_Unit

English

For nonzero f, f = divXPowOrder f if and only if f is a unit.

Русский

Для непустого f верно: f = divXPowOrder f ⇔ f является единицей.

LaTeX

$$$ f \neq 0 \Rightarrow (f = divXPowOrder f \iff IsUnit f). $$$

Lean4

theorem eq_divided_by_X_pow_order_Iff_Unit {f : k⟦X⟧} (hf : f ≠ 0) : f = divXPowOrder f ↔ IsUnit f :=
  ⟨fun h ↦ by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h ↦
    by
    have : f.order = 0 := by simp [order_zero_of_unit h]
    conv_lhs => rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero, pow_zero, one_mul]⟩

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