English
In a separable extension, the q^n-th power of a basis element remains within the span.
Русский
В разделяемом расширении q^n-й степени элемент базиса продолжает принадлежать порождению.
LaTeX
$$$b_i^{q^n} \in \operatorname{span}\{b_j^{q^n}\}$$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable,
then $[K:F]_s = [K:E]_s$.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it. -/
theorem sepDegree_eq_of_isPurelyInseparable [IsPurelyInseparable F E] : sepDegree F K = sepDegree E K :=
by
convert sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)
haveI : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F (separableClosure.separableClosure_eq_bot E K)]
exact
(separableClosure F (separableClosure E K)).equivMap
(IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq
