Unit_of_divided_by_X_pow_order_nonzero

English

For nonzero f, the value of the unit associated to divXPowOrder f equals divXPowOrder f itself.

Русский

Для непустого f значение связанной единицы равно самому divXPowOrder f.

LaTeX

$$$ (Unit\_of\_divided\_by\_X\_pow\_order f).val = divXPowOrder f. $$$

Lean4

theorem Unit_of_divided_by_X_pow_order_nonzero {f : k⟦X⟧} (hf : f ≠ 0) :
    ↑(Unit_of_divided_by_X_pow_order f) = divXPowOrder f := by
  simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]

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