Powers in the unit group of a valuation subring

A nonzero power of a field unit has valuation one exactly when that unit does. Consequently a root in the field of a unit of the valuation subring is itself a unit of the valuation subring. This permits local power equations to be read in the unit group.

theorem Valuation.pow_mem_unitGroup_iff {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) {n : ℕ} (hn : n ≠ 0) {x : Kˣ} : x ^ n ∈ v.valuationSubring.unitGroup ↔ x ∈ v.valuationSubring.unitGroup

A field unit belongs to the unit group of the valuation subring if and only if one of its nonzero powers does.