New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: characterize roots of unity in cyclotomic extensions #10710
Conversation
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
Please update the top post, since the name bors d+ |
✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
We add `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder`: If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of `ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n` such that `x = ζ^r` or `x = -ζ^r`. From flt-regular - [x] depends on: #11235
Pull request successfully merged into master. Build succeeded: |
We add `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder`: If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of `ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n` such that `x = ζ^r` or `x = -ζ^r`. From flt-regular - [x] depends on: #11235
We add `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder`: If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of `ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n` such that `x = ζ^r` or `x = -ζ^r`. From flt-regular - [x] depends on: #11235
We add `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder`: If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of `ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n` such that `x = ζ^r` or `x = -ζ^r`. From flt-regular - [x] depends on: #11235
We add `IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder`: If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of `ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n` such that `x = ζ^r` or `x = -ζ^r`. From flt-regular - [x] depends on: #11235
We add
IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder
: Ifx
is a root of unity (spelled asIsOfFinOrder x
) in ann
-th cyclotomic extension ofℚ
, wheren
is odd, andζ
is a primitiven
-th root of unity, then there existsr < n
such thatx = ζ^r
orx = -ζ^r
.From flt-regular