English
The order of φ equals the emultiplicity of X in φ.
Русский
Порядок φ равен эмплитности X в φ.
LaTeX
$$$\operatorname{order}(\phi) = \operatorname{emultiplicity}(X,\phi)$$$
Lean4
theorem order_eq_emultiplicity_X {R : Type*} [Semiring R] (φ : R⟦X⟧) : order φ = emultiplicity X φ := by
classical
rcases eq_or_ne φ 0 with (rfl | hφ)
· simp
cases ho : order φ with
| top => simp [hφ] at ho
| coe n =>
have hn : φ.order.toNat = n := by simp [ho]
rw [← hn, eq_comm]
apply le_antisymm _
· apply le_emultiplicity_of_pow_dvd
apply X_pow_order_dvd
· apply Order.le_of_lt_add_one
rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]
rintro ⟨ψ, H⟩
have := congr_arg (coeff n) H
rw [X_pow_mul, coeff_mul_of_lt_order, ← hn] at this
· exact coeff_order hφ this
· rw [X_pow_eq, order_monomial]
split_ifs
· simp
· rw [← hn, ENat.coe_lt_coe]
simp
