count_zpow — Mathlib

English

For any integer n, count(K, v, I^n) = n · 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

/-- `val_v(Iⁿ) = n*val_v(I)` for every `n ∈ ℤ`. -/
theorem count_zpow (n : ℤ) (I : FractionalIdeal R⁰ K) : count K v (I ^ n) = n * count K v I :=
  by
  obtain n | n := n
  · rw [ofNat_eq_coe, zpow_natCast]
    exact count_pow K v n I
  · rw [negSucc_eq, count_neg_zpow, ← Int.natCast_succ, zpow_natCast, count_pow]
    ring

Похожие утверждения