isSolvable — Mathlib

English

Every solvable-by-radical element α in solvableByRad F E has a solvable Galois group: Gal(minpoly F α).

Русский

Каждый элемент α из solvableByRad F E, разрешимый радикалами, имеет разрешимую Галуа-группу: Gal(minpoly F α).

LaTeX

$$$$\forall α \in solvableByRad F E,\ IsSolvable(\minpoly F α).Gal$$$$

Lean4

theorem isSolvable (α : solvableByRad F E) : IsSolvable (minpoly F α).Gal :=
  by
  revert α
  apply solvableByRad.induction
  · exact fun α => by rw [minpoly.eq_X_sub_C (solvableByRad F E)]; exact gal_X_sub_C_isSolvable α
  ·
    exact fun α β =>
      induction2
        (add_mem (subset_adjoin F _ (Set.mem_insert α _))
          (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))
  · exact fun α => induction1 (neg_mem (mem_adjoin_simple_self F α))
  ·
    exact fun α β =>
      induction2
        (mul_mem (subset_adjoin F _ (Set.mem_insert α _))
          (subset_adjoin F _ (Set.mem_insert_of_mem α (Set.mem_singleton β))))
  · exact fun α => induction1 (inv_mem (mem_adjoin_simple_self F α))
  · exact fun α n => induction3

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