ValuationTheory.DiscreteValuationField.DVF.finite_primePowerRoots_of_finiteExtension
Every finite field extension of a mixed-characteristic DVF has only finitely many prime-power roots. No extension valuation is assumed.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]Lean source · statement
theorem DVF.finite_primePowerRoots_of_finiteExtension [CharZero K] (base : DVF K)
(p : ℕ) [Fact p.Prime] [CharP base.residueField p] :
Set.Finite {ζ : L | ∃ n : ℕ, ζ ^ (p ^ n) = 1}