English
If f is weakly Eisenstein at a prime-ideal 𝓟 in a commutative semiring R, then for any ring homomorphism φ : R → S, the map φ applied to f is weakly Eisenstein at 𝓟 mapped to φ(𝓟) in S.
Русский
Пусть f является слабоэллиптическим (weakly Eisenstein) на гладком идеале 𝓟 в R. Тогда для любой гомоморфной пары φ: R → S отображение f под φ сохраняет свойство слабой Эйзенштейновости на образе 𝓟: 𝓟.map φ.
LaTeX
$$f.IsWeaklyEisensteinAt 𝓟 → φ: R →+* S → (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ)$$
Lean4
theorem mul (hf : f.IsWeaklyEisensteinAt 𝓟) (hf' : f'.IsWeaklyEisensteinAt 𝓟) : (f * f').IsWeaklyEisensteinAt 𝓟 :=
by
rw [isWeaklyEisensteinAt_iff] at hf hf' ⊢
intro n hn
rw [coeff_mul]
refine sum_mem _ fun x hx ↦ ?_
rcases lt_or_ge x.1 f.natDegree with hx1 | hx1
· exact mul_mem_right _ _ (hf hx1)
replace hx1 : x.2 < f'.natDegree := by
by_contra!
rw [HasAntidiagonal.mem_antidiagonal] at hx
replace hn := hn.trans_le natDegree_mul_le
linarith
exact mul_mem_left _ _ (hf' hx1)
