Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic #5335

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic #5335

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
d5a6a57
feat: port NumberTheory.Cyclotomic.Basic
riccardobrasca Jun 21, 2023
444aeca
Initial file copy from mathport
riccardobrasca Jun 21, 2023
501b137
automated fixes
riccardobrasca Jun 21, 2023
aaf4c8a
first fixes
riccardobrasca Jun 21, 2023
cd49233
progress
riccardobrasca Jun 21, 2023
c91cdab
Merge remote-tracking branch 'origin/master' into port/NumberTheory.C…
ChrisHughes24 Jun 21, 2023
937604d
fix one proof
ChrisHughes24 Jun 21, 2023
efe1b6c
more fixes
ChrisHughes24 Jun 21, 2023
59fc03f
more fixes
ChrisHughes24 Jun 21, 2023
2cbbd8e
small fix
ChrisHughes24 Jun 21, 2023
cb37e59
trivial fixes
riccardobrasca Jun 21, 2023
c491103
this should compile
riccardobrasca Jun 21, 2023
4b545a8
names
riccardobrasca Jun 21, 2023
b822373
doc
riccardobrasca Jun 21, 2023
430ec14
Update Mathlib/NumberTheory/Cyclotomic/Basic.lean
riccardobrasca Jun 22, 2023
a5f5d66
use capital letter
riccardobrasca Jun 22, 2023
d2fe6fa
add note
riccardobrasca Jun 22, 2023
25d2035
another note
riccardobrasca Jun 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2277,6 +2277,7 @@ import Mathlib.NumberTheory.BernoulliPolynomials
import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
import Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.NumberTheory.Dioph
import Mathlib.NumberTheory.DiophantineApproximation
import Mathlib.NumberTheory.Divisors
Expand Down
Loading
Loading