X_pow_order_dvd

Mathlib.RingTheory.PowerSeries.Order

URI: https://scilib.ai/kg/mathlib#PowerSeries.X_pow_order_dvd

English

The X-power congruence X^{order(f).toNat} divides f.

Русский

X^{order(f).toNat} делит f.

LaTeX

$$$X^{\operatorname{order}(f).toNat} \mid f$$$

Lean4

theorem X_pow_order_dvd : X ^ φ.order.toNat ∣ φ := by simpa only [X_pow_dvd_iff] using coeff_of_lt_order_toNat

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru