English
Under the same assumptions as contraction_degree_eq_or_insep, the degrees of two separable contractions agree when their expanded forms match.
Русский
При тех же предпосылках, что и в contraction_degree_eq_or_insep, степени двух разделимых конракций совпадают, если их раз expanding совпадает.
LaTeX
$$$\\forall q\\; [hq : NeZero\\ q]\\ [CharP\\ F\\ q]\\ (g\\ g' : F[X]) (m\\ m' : \\mathbb{N}),\\; expand\\ F (q^m) g = expand\\ F (q^{m'}) g' \\Rightarrow g.natDegree = g'.natDegree$$$
Lean4
/-- The separable degree equals the degree of any separable contraction, i.e., it is unique. -/
theorem degree_eq [hF : ExpChar F q] (g : F[X]) (hg : IsSeparableContraction q f g) : g.natDegree = hf.degree :=
by
cases hF
· rcases hg with ⟨_, m, hm⟩
rw [one_pow, expand_one] at hm
rw [hf.eq_degree, hm]
· rcases hg with ⟨hg, m, hm⟩
let g' := Classical.choose hf
obtain ⟨hg', m', hm'⟩ := Classical.choose_spec hf
haveI : Fact q.Prime := ⟨by assumption⟩
refine contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'
rw [hm, hm']
