English
If two expansions along the positive characteristic of two separable polynomials g and g' agree, then their degrees are equal.
Русский
Если два разложения по положительной характеристике пары разделимых многочленов g и g' совпадают, то их степени равны.
LaTeX
$$$\\forall q\\; [hq : NeZero\\ q]\\ [CharP\\ F\\ q]\\ (g\\ g' : F[X])\\ (m\\ m' : \\mathbb{N}),\\; (h\\_expand : expand\\ F (q^m)\\ g = expand\\ F (q^{m'})\\ g') \\Rightarrow g.natDegree = g'.natDegree$$$
Lean4
/-- If two expansions (along the positive characteristic) of two separable polynomials `g` and `g'`
agree, then they have the same degree. -/
theorem contraction_degree_eq_or_insep [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
(h_expand : expand F (q ^ m) g = expand F (q ^ m') g') (hg : g.Separable) (hg' : g'.Separable) :
g.natDegree = g'.natDegree := by
wlog hm : m ≤ m'
· exact (this q g' g m' m h_expand.symm hg' hg (le_of_not_ge hm)).symm
obtain ⟨s, rfl⟩ := exists_add_of_le hm
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand
subst h_expand
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
· rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
· rw [natDegree_expand, pow_zero, mul_one]
