lift_rank_mul_lift_sepDegree_of_isSeparable

English

Iterated q-power maps preserve linear independence and spanning for a basis in a separable setting.

Русский

Итеративные q-поднятия сохраняют линейную независимость и порождение для базиса в сепарируемой обстановке.

LaTeX

$$$\text{linearIndependent}(b_i^{q^n})\;\wedge\;\operatorname{span}(b_i^{q^n})=E$$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is separable,
then $[E:F] [K:E]_s = [K:F]_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 lift_rank_mul_lift_sepDegree_of_isSeparable [Algebra.IsSeparable F E] :
    Cardinal.lift.{w} (Module.rank F E) * Cardinal.lift.{v} (sepDegree E K) = Cardinal.lift.{v} (sepDegree F K) :=
  by
  rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]
  exact lift_rank_mul_lift_rank F E (separableClosure E K)

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