upstreaming some results about `UInt*`

Stream: mathlib4

[Kim Morrison]

I'm moving some results about UInt* from Mathlib up to Lean in #4231.

Hopefully this will leave the only results about UInt* in Mathlib as results about Mathlib notions, e.g. CommRing and NeZero.

[Yury G. Kudryashov]

lean#4231