English
For any nonzero I there exists a representation I = a^{-1} J with some a ∈ R and an ideal J, such that count(K, v, I) equals count(K, v, J) − count(K, v, a).
Русский
Для любого ненулевого I существует представление I = a^{-1} J с некоторым a ∈ R и идеалом J, такое что count(K, v, I) = count(K, v, J) − count(K, v, a).
LaTeX
$$$$ \\exists a,J:\\ I = a^{-1}J \\ \\Rightarrow\\ \\operatorname{count}(K,v,I)=\\operatorname{count}(K,v,J)-\\operatorname{count}(K,v,a). $$$$
Lean4
/-- For nonzero `I, I'`, `val_v(I*I') = val_v(I) + val_v(I')`. If `I` or `I'` is zero, then
`val_v(I*I') = 0`. -/
theorem count_mul' (I I' : FractionalIdeal R⁰ K) [Decidable (I ≠ 0 ∧ I' ≠ 0)] :
count K v (I * I') = if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0 :=
by
split_ifs with h
· exact count_mul K v h.1 h.2
· rw [← mul_ne_zero_iff, not_ne_iff] at h
rw [h, count_zero]
