Skip to content

Commit

Permalink
feat: port NumberTheory.Cyclotomic.Basic (#5335)
Browse files Browse the repository at this point in the history
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
  • Loading branch information
2 people authored and kbuzzard committed Jul 6, 2023
1 parent 62a55ad commit 9aee20e
Show file tree
Hide file tree
Showing 3 changed files with 754 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2283,6 +2283,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

0 comments on commit 9aee20e

Please sign in to comment.