Yamaguchi26AbfaithfulGalois.finite_primePowerRoots_of_mixedChar
Lemma 3.1 of Yamaguchi, arXiv:2610.05634v1: a mixed-characteristic discrete valuation bounds the exponent of the p-power roots of unity in the field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
universe u vLean source · statement
theorem finite_primePowerRoots_of_mixedChar
{K : Type u} [Field K] [CharZero K]
(base : DVF.{u, v} K) (p : ℕ) [Fact p.Prime]
[CharP base.residueField p] :
Set.Finite {ζ : K | ∃ n : ℕ, ζ ^ (p ^ n) = 1}