isCyclic — Mathlib

English

A quadratic extension has a cyclic Galois group.

Русский

Квадратичное расширение имеет циклическую группу Галуа.

LaTeX

$$For a quadratic extension, the Galois group is cyclic of order 2: $\mathrm{Gal}(K/F) \cong C_2$.$$

Lean4

/-- A quadratic extension has cyclic Galois group.
-/
instance isCyclic : IsCyclic (K ≃ₐ[F] K) :=
  by
  have := finrank_eq_two F K ▸ AlgEquiv.card_le
  rw [← Nat.card_eq_fintype_card] at this
  interval_cases h : Nat.card (K ≃ₐ[F] K)
  · simp_all
  · exact @isCyclic_of_subsingleton _ _ (Finite.card_le_one_iff_subsingleton.mp h.le)
  · exact isCyclic_of_prime_card h

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