Skip to content

Commit

Permalink
fix: typo in module doc of NumberTheory/Cyclotomic/Basic (#11670)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn authored and callesonne committed Apr 22, 2024
1 parent 4e199b9 commit 20819c2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/Cyclotomic/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ primitive roots of unity, for all `n ∈ S`.
`B` is a finite `A`-algebra.
* `IsCyclotomicExtension.numberField` : a finite cyclotomic extension of a number field is a
number field.
* `IsCyclotomicExtension.splitting_field_X_pow_sub_one` : if `IsCyclotomicExtension {n} K L`,
* `IsCyclotomicExtension.isSplittingField_X_pow_sub_one` : if `IsCyclotomicExtension {n} K L`,
then `L` is the splitting field of `X ^ n - 1`.
* `IsCyclotomicExtension.splitting_field_cyclotomic` : if `IsCyclotomicExtension {n} K L`,
then `L` is the splitting field of `cyclotomic n K`.
Expand Down

0 comments on commit 20819c2

Please sign in to comment.