English
For any nonzero J ⊆ R, count(K, v, coeIdeal(J)) equals (Associates.mk v.asIdeal).count (Associates.mk J).factors.
Русский
Для любого ненулевого J ⊆ R, count(K, v, coeIdeal(J)) равен количеству факторов (Associates.mk v.asIdeal) относительно (Associates.mk J).factors.
LaTeX
$$$$ \\operatorname{count}(K,v, \\mathrm{coeIdeal}(J)) = (\\mathrm{Associates.mk}\\,v.asIdeal).\\mathrm{count} (\\mathrm{Associates.mk}\\,J).\\mathrm{factors}. $$$$
Lean4
theorem count_coe {J : Ideal R} (hJ : J ≠ 0) :
count K v J = (Associates.mk v.asIdeal).count (Associates.mk J).factors :=
by
rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self, Nat.cast_eq_zero, ←
Ideal.one_eq_top, Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible]
· simpa only [ne_eq, coeIdeal_eq_zero]
· simp only [map_one, inv_one, spanSingleton_one, one_mul]
