feat: port RingTheory.WittVector.IsPoly (#4851)

This file contains a couple of tactics. I ported everything that is not a tactic and added an "attributes" file. My plan is to try to develop the tactics while porting a file that actually uses them.
leanprover-community · Jun 8, 2023 · 5d80868 · 5d80868
1 parent ac5fb5c
commit 5d80868
Show file tree

Hide file tree

Showing 3 changed files with 665 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2429,8 +2429,10 @@ import Mathlib.RingTheory.Valuation.Quotient
 import Mathlib.RingTheory.Valuation.ValuationRing
 import Mathlib.RingTheory.WittVector.Basic
 import Mathlib.RingTheory.WittVector.Defs
+import Mathlib.RingTheory.WittVector.IsPoly
 import Mathlib.RingTheory.WittVector.StructurePolynomial
 import Mathlib.RingTheory.WittVector.Teichmuller
+import Mathlib.RingTheory.WittVector.WittAttributes
 import Mathlib.RingTheory.WittVector.WittPolynomial
 import Mathlib.RingTheory.ZMod
 import Mathlib.SetTheory.Cardinal.Basic