doc(field_theory/abel_ruffini): update module doc (#10426)

leanprover-community · Nov 23, 2021 · 7958251 · 7958251
1 parent 2b75493
commit 7958251
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/field_theory/abel_ruffini.lean b/src/field_theory/abel_ruffini.lean
@@ -16,12 +16,12 @@ by radicals, then its minimal polynomial has solvable Galois group.
 
 ## Main definitions
 
-* `SBF F E` : the intermediate field of solvable-by-radicals elements
+* `solvable_by_rad F E` : the intermediate field of solvable-by-radicals elements
 
 ## Main results
 
-* `solvable_gal_of_solvable_by_rad` : the minimal polynomial of an element of `SBF F E` has
-solvable Galois group
+* the Abel-Ruffini Theorem `solvable_by_rad.is_solvable'` : An irreducible polynomial with a root
+that is solvable by radicals has a solvable Galois group.
 -/
 
 noncomputable theory