English
The set of associated primes of the product module M × M' is the union of the associated primes of M and those of M'.
Русский
Множество ассоциированных простых модуля M × M' равно объединению ассоциированных простых для M и для M'.
LaTeX
$$$$\operatorname{associatedPrimes}(R, M \times M') = \operatorname{associatedPrimes}(R, M) \cup \operatorname{associatedPrimes}(R, M'). $$$$
Lean4
/-- The set of associated primes of the product of two modules is equal to
the union of those of the two modules. -/
@[stacks 02M3 "third part"]
theorem prod : associatedPrimes R (M × M') = associatedPrimes R M ∪ associatedPrimes R M' :=
(subset_union_of_exact LinearMap.inl_injective .inl_snd).antisymm
(Set.union_subset_iff.2 ⟨subset_of_injective LinearMap.inl_injective, subset_of_injective LinearMap.inr_injective⟩)
