Documentation

Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Instances for HasEnoughRootsOfUnity #

We provide an instance for HasEnoughRootsOfUnity F n when F is an algebraically closed field and n is not divisible by the characteristic. In particular, when F has characteristic zero, this hold for all n ≠ 0.

An algebraically closed field F satisfies HasEnoughRootsOfUnity F n for all n that are not divisible by the characteristic of F.