X_pow_order_mul_divXPowOrder — Mathlib

English

The product X^{order(f).toNat} · divXPowOrder f equals f.

Русский

Произведение X^{order(f).toNat} · divXPowOrder f равно f.

LaTeX

$$$X^{\operatorname{order}(f).{\text{toNat}}} \cdot \operatorname{divXPowOrder} f = f$$$

Lean4

theorem X_pow_order_mul_divXPowOrder {f : R⟦X⟧} : X ^ f.order.toNat * divXPowOrder f = f :=
  by
  ext n
  rw [coeff_X_pow_mul']
  split_ifs with h
  · simp [h]
  · push_neg at h
    rw [coeff_of_lt_order_toNat _ h]

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