isSimpleOrder_of_finrank_prime — Mathlib

English

If the finrank of E over F is a prime number, then the lattice of intermediate fields is simple (has no nontrivial proper subobjects).

Русский

Если размерность расширения E/F является простым числом, то отпуск промежуточных полей образует простое множество (нет ненулевых допустимых подполей).

LaTeX

$$ hp : Nat.Prime (Module.finrank F E) → IsSimpleOrder (IntermediateField F E)$$

Lean4

theorem isSimpleOrder_of_finrank_prime (hp : Nat.Prime (Module.finrank F E)) : IsSimpleOrder (IntermediateField F E) :=
  by
  refine { toNontrivial := ?_, eq_bot_or_eq_top := ?_ }
  · exact ⟨⊥, ⊤, fun h ↦ Nat.prime_one_false (bot_eq_top_iff_finrank_eq_one.mp h ▸ hp)⟩
  · intro K
    simpa [← toSubalgebra_strictMono.apply_eq_bot_iff, ← toSubalgebra_strictMono.apply_eq_top_iff] using
      (Subalgebra.isSimpleOrder_of_finrank_prime _ _ hp).eq_bot_or_eq_top K.toSubalgebra

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