two_le_deg — Mathlib

English

For each i, the number of embeddings X_i is at least 2, i.e. 2 ≤ #(X_i).

Русский

Для каждого i имеется по крайней мере две вложения, то есть 2 ≤ #(X_i).

LaTeX

$$$$2 \\le \\#(X_i)$$$$

Lean4

theorem two_le_deg (i : ι) : 2 ≤ #(X i) :=
  by
  rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 (nat_lt_aleph0 _) (deg_lt_aleph0 i), toNat_natCast, ← Nat.card, ←
    finSepDegree, finSepDegree_eq_finrank_of_isSeparable, Nat.succ_le]
  by_contra!
  obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)
  refine (isLeast_leastExt i).1 (hx ▸ ?_)
  exact x.2

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