English
For a separable extension F⊆E, the number of F-embeddings of E into an algebraic closure Ē equals 2 raised to the rank of E over F.
Русский
Для сепарабельного расширения F⊆E число вложений F-эмбедингов E в алг Closure Ē равно 2^{rank_F E}.
LaTeX
$$$\\#(\\mathrm{Field Emb } F E) = 2^{\\operatorname{rank}_F(E)}$$$
Lean4
theorem cardinal_eq_two_pow_rank [Algebra.IsSeparable F E] (rank_inf : ℵ₀ ≤ Module.rank F E) :
#(Field.Emb F E) = 2 ^ Module.rank F E := by
haveI := Fact.mk rank_inf
rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]
apply le_antisymm
· rw [← power_eq_two_power rank_inf (nat_lt_aleph0 2).le rank_inf]
conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
exact prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le
· conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
exact prod_le_prod _ _ Emb.Cardinal.two_le_deg
