English
For a natural exponent n, count(K, v, I^n) equals n times count(K, v, I).
Русский
Для натурального показателя n выполняется: count(K, v, I^n) = n · count(K, v, I).
LaTeX
$$$$ \\operatorname{count}(K,v,I^n) = n \\cdot \\operatorname{count}(K,v,I)$$$$
Lean4
/-- For every `n ∈ ℕ` and every ideal `I`, `val_v(I^n) = n*val_v(I)`. -/
theorem count_pow (n : ℕ) (I : FractionalIdeal R⁰ K) : count K v (I ^ n) = n * count K v I := by
induction n with
| zero => rw [pow_zero, ofNat_zero, zero_mul, count_one]
| succ n h =>
classical rw [pow_succ, count_mul']
by_cases hI : I = 0
· have h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0) := by
rw [not_and', not_not, ne_eq]
intro h
exact absurd hI h
rw [if_neg h_neg, hI, count_zero, mul_zero]
· rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add, Nat.cast_one]
ring
