English
For any natural n, the supDegree of p^n with respect to D equals n times supDegree_D(p), provided certain base conditions (D injective, hadd additive, p monic and other mild hypotheses).
Русский
Для целого n выполняется, что supDegree_D(p^n) = n · supDegree_D(p) при заданных условиях (инъективность D, аддитивность hadd, p моничен и т. д.).
LaTeX
$$$$\operatorname{supDegree}_D(p^n) = n \cdot \operatorname{supDegree}_D(p).$$$$
Lean4
theorem supDegree_pow (hzero : D 0 = 0) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hD : D.Injective) [Nontrivial R]
(hp : p.Monic D) : (p ^ n).supDegree D = n • p.supDegree D := by
induction n with
| zero => rw [pow_zero, zero_nsmul, one_def, supDegree_single 0 1, if_neg one_ne_zero, hzero]
| succ n ih => rw [pow_succ', (hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero, ih, succ_nsmul']
