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: port NumberTheory.ClassNumber.Finite #5337
Conversation
Genora51
commented
Jun 21, 2023
Currently struggling with a couple of errors that I can't seem to resolve, plus a timeout issue on |
Can you please fix the conflict? Not sure I have time today, but I will have a look tomorrow. |
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
553d393
to
582df94
Compare
@riccardobrasca I've rebased onto latest |
|
||
attribute [-instance] Real.decidableEq | ||
|
||
set_option maxHeartbeats 800000 in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This proof is rather slow. Maybe @Vierkantor wants to have a look at it (but it is already slow in mathlib3).
@Genora51 I think this is now green. I didn't fix any doc/name. |
finite extension `L` of `K = Frac(R)` is finite if there is an admissible | ||
absolute value. | ||
|
||
See also `class_group.fintype_of_admissible_of_algebraic` where `L` is an |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This name is still the mathlib3 name.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suggest we look at speedups in follow-up PRs. The file looks good syntactically. Thanks 🎉
bors merge
Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>