Positive divisor degree of a power

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_pow (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (m : ℕ) : finiteExtensionPositiveDegree K L (x ^ m) = m * finiteExtensionPositiveDegree K L x

The positive degree of a principal divisor scales by the exponent.