feat: port RingTheory.RootsOfUnity.Basic (#4677)

Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · Jun 7, 2023 · 55822ef · 55822ef
1 parent 3d3a468
commit 55822ef
Show file tree

Hide file tree

Showing 2 changed files with 1,004 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2379,6 +2379,7 @@ import Mathlib.RingTheory.QuotientNilpotent
 import Mathlib.RingTheory.QuotientNoetherian
 import Mathlib.RingTheory.ReesAlgebra
 import Mathlib.RingTheory.RingInvo
+import Mathlib.RingTheory.RootsOfUnity.Basic
 import Mathlib.RingTheory.SimpleModule
 import Mathlib.RingTheory.Subring.Basic
 import Mathlib.RingTheory.Subring.Pointwise