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.

Author: adomani

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