count_inv — Mathlib

English

The count of the inverse fractional ideal satisfies count(K, v, I^{-1}) = − count(K, v, I).

Русский

Значение count для обратного дробного идеала: count(K, v, I^{-1}) = − count(K, v, I).

LaTeX

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

Lean4

theorem count_inv (I : FractionalIdeal R⁰ K) : count K v (I⁻¹) = -count K v I := by
  rw [← zpow_neg_one, count_neg_zpow K v (1 : ℤ) I, zpow_one]

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