count_neg_zpow — Mathlib

English

For any integer n and I, count(K, v, I^{−n}) = − count(K, v, I^n).

Русский

Для любого целого n и I выполняется count(K, v, I^{−n}) = − count(K, v, I^n).

LaTeX

$$$$ \\operatorname{count}(K,v,I^{-n}) = -\\operatorname{count}(K,v,I^{n}). $$$$

Lean4

/-- `val_v(I⁻ⁿ) = -val_v(Iⁿ)` for every `n ∈ ℤ`. -/
theorem count_neg_zpow (n : ℤ) (I : FractionalIdeal R⁰ K) : count K v (I ^ (-n)) = -count K v (I ^ n) :=
  by
  by_cases hI : I = 0
  · by_cases hn : n = 0
    · rw [hn, neg_zero, zpow_zero, count_one, neg_zero]
    · rw [hI, zero_zpow n hn, zero_zpow (-n) (neg_ne_zero.mpr hn), count_zero, neg_zero]
  · rw [eq_neg_iff_add_eq_zero, ← count_mul K v (zpow_ne_zero _ hI) (zpow_ne_zero _ hI), ← zpow_add₀ hI, neg_add_cancel,
      zpow_zero]
    exact count_one K v

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