cardinal_separableClosure — Mathlib

English

There is no increase in the number of F-embeddings when passing to the separable closure inside E.

Русский

Число вложений F в separableClosure(F,E) не больше, чем в E.

LaTeX

$$$\#(\mathrm{Field.Emb}\, F\, \mathrm{separableClosure}\, F E) = #(\mathrm{Field.Emb}\, F E)$$$

Lean4

theorem cardinal_separableClosure [Algebra.IsAlgebraic F E] :
    #(Field.Emb F <| separableClosure F E) = #(Field.Emb F E) := by
  rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq, mk_prod, mk_eq_one (Emb _ E), lift_one,
    mul_one, lift_id]

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