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 committed Mar 25, 2024
1 parent a251ad4 commit 103d868
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/Cyclotomic/Basic.lean
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 103d868

Please sign in to comment.