English
If I ≠ 0, then count(K, v, I) equals count(K, v, J) − count(K, v, a) for some representation I = a^{-1} J with a ∈ R and J an ideal.
Русский
Если I ≠ 0, тогда count(K, v, I) равно count(K, v, J) − count(K, v, a) для какого-либо представления I = a^{-1} J.
LaTeX
$$$$\\text{If } I \\neq 0, \\quad \\operatorname{count}(K,v,I)= \\operatorname{count}(K,v,J) - \\operatorname{count}(K,v,a) \\text{ for some } I = a^{-1}J.$$$$
Lean4
theorem count_ne_zero {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) :
count K v I =
((Associates.mk v.asIdeal).count (Associates.mk (choose (choose_spec (exists_eq_spanSingleton_mul I)))).factors -
(Associates.mk v.asIdeal).count
(Associates.mk (Ideal.span {choose (exists_eq_spanSingleton_mul I)})).factors :
ℤ) :=
by simp only [count, dif_neg hI]
