LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_primePower_root_of_field_root
A prime-power root in the field lifts to a root in the actual first principal-unit group; its underlying field element is the prescribed root.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]Lean source · statement
theorem exists_primePower_root_of_field_root
(F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
(p : ℕ) [Fact p.Prime] [hres : CharP F.residueField p]
(s : ℕ) (y : K) (u : higherPrincipalUnitGroup F 1)
(hy : y ^ (p ^ s) = (((u : F.valuationSubringˣ) : F.valuationSubring) : K)) :
∃ z : higherPrincipalUnitGroup F 1,
(((z : F.valuationSubringˣ) : F.valuationSubring) : K) = y ∧
z ^ (p ^ s) = u