theorem
L26 ↗existsUnique_rootScale
EtaleFundamentalGroups.Kummer.existsUnique_rootScale
Two nonzero roots of the same prime-to-characteristic power differ by a unique root of unity in the separably closed base field.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace EtaleFundamentalGroups.KummerLean source · statement
theorem existsUnique_rootScale {K : Type u} [Field K] [IsSepClosed K]
{Ω : Type v} [Field Ω] (ι : K →+* Ω) (n : ℕ+)
(hn : IsUnit ((n : ℕ) : K)) (x y : Ω) (hx : x ≠ 0)
(hxy : x ^ (n : ℕ) = y ^ (n : ℕ)) :
∃! ζ : rootsOfUnity (n : ℕ) K, ι ((ζ : Kˣ) : K) * x = y