English
If a Finset s of indices has i in s, and each f(y) is primary with radicals all equal to radical of f(i), then the infimum over s of f is primary.
Русский
Если финитный набор индексов s содержит i, и все f(y) примарны, радикалы которых равны радикалу f(i), то infimum s.inf f примарен.
LaTeX
$$$i \in s \\Rightarrow \\big( \forall y \in s, (f(y)).IsPrimary \big) \\Rightarrow \\big( \forall y \in s, \operatorname{radical}(f(y)) = \operatorname{radical}(f(i)) \big) \\Rightarrow \\ (s.inf f).IsPrimary$$
Lean4
theorem absNorm_under_prime (P : Ideal R) [P.IsPrime] [NeZero P] : (absNorm (under ℤ P)).Prime :=
by
rw [Nat.prime_iff_prime_int, ← span_singleton_prime, Int.ideal_span_absNorm_eq_self]
· infer_instance
· refine Int.natCast_ne_zero.mpr <| absNorm_eq_zero_iff.not.mpr ?_
have : P ≠ ⊥ := NeZero.ne _
contrapose! this
exact eq_bot_of_comap_eq_bot this
