sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'

English

The map C sends each scalar to the corresponding constant rational function.

Русский

Отображение C отправляет каждую скалярную величину в соответствующую константную рациональную функцию.

LaTeX

$$C : K →+* RatFunc K$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any intermediate field `S` of `K / F` such that `S / F` is algebraic, the `E(S) / E` and
`S / F` have the same separable degree. -/
theorem sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable' (S : IntermediateField F K) [Algebra.IsAlgebraic F S]
    [IsPurelyInseparable F E] : sepDegree E (adjoin E (S : Set K)) = sepDegree F S :=
  by
  have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self]
  have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set K)
  rwa [adjoin_self] at this

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