English
If I and I′ are nonzero fractional ideals, then count(K, v, I I′) = count(K, v, I) + count(K, v, I′).
Русский
Если I и I′ — ненулевые дробные идеалы, то count(K, v, II′) = count(K, v, I) + count(K, v, I′).
LaTeX
$$$$\\operatorname{count}(K,v, I I') = \\operatorname{count}(K,v,I) + \\operatorname{count}(K,v,I').$$$$
Lean4
/-- For nonzero `I, I'`, `val_v(I*I') = val_v(I) + val_v(I')`. -/
theorem count_mul {I I' : FractionalIdeal R⁰ K} (hI : I ≠ 0) (hI' : I' ≠ 0) :
count K v (I * I') = count K v I + count K v I' := by
classical
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
obtain ⟨a, J, ha, haJ⟩ := exists_eq_spanSingleton_mul I
have ha_ne_zero : Associates.mk (Ideal.span { a } : Ideal R) ≠ 0 := by
rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact ha
have hJ_ne_zero : Associates.mk J ≠ 0 := Associates.mk_ne_zero.mpr (ideal_factor_ne_zero hI haJ)
obtain ⟨a', J', ha', haJ'⟩ := exists_eq_spanSingleton_mul I'
have ha'_ne_zero : Associates.mk (Ideal.span { a' } : Ideal R) ≠ 0 := by
rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact ha'
have hJ'_ne_zero : Associates.mk J' ≠ 0 := Associates.mk_ne_zero.mpr (ideal_factor_ne_zero hI' haJ')
have h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J') := by
rw [haJ, haJ', mul_assoc, mul_comm (J : FractionalIdeal R⁰ K), mul_assoc, ← mul_assoc,
spanSingleton_mul_spanSingleton, coeIdeal_mul, RingHom.map_mul, mul_inv, mul_comm (J : FractionalIdeal R⁰ K)]
rw [count_well_defined K v hI haJ, count_well_defined K v hI' haJ',
count_well_defined K v (mul_ne_zero hI hI') h_prod, ← Associates.mk_mul_mk,
Associates.count_mul hJ_ne_zero hJ'_ne_zero hv, ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk,
Associates.count_mul ha_ne_zero ha'_ne_zero hv]
push_cast
ring
