finSepDegree_eq_zero_of_transcendental

English

If E/F is a transcendental extension, then the separable degree finSepDegree(F,E) equals 0, i.e., there are infinitely many embeddings.

Русский

Если расширение E/F трансцендентно, то финальная сепарабельная степень равна 0, то есть существует бесконечное множество вложений.

LaTeX

$$$\operatorname{finSepDegree}(F,E) = 0$$$

Lean4

/-- If the field extension `E / F` is transcendental, then `Field.finSepDegree F E = 0`, which
actually means that `Field.Emb F E` is infinite (see `Field.infinite_emb_of_transcendental`). -/
theorem finSepDegree_eq_zero_of_transcendental [Algebra.Transcendental F E] : finSepDegree F E = 0 :=
  Nat.card_eq_zero_of_infinite

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