mul — Mathlib

English

If f and g are distinguished at I, then their product f*g is distinguished at I.

Русский

Если f и g разделены по характеристике I, то произведение f*g тоже распределимо по I.

LaTeX

$$$\\forall f,g\\in R[X]\\; (f.IsDistinguishedAt I) \\to (g.IsDistinguishedAt I) \\to (f*g).IsDistinguishedAt I$$$

Lean4

theorem mul {f f' : R[X]} {I : Ideal R} (hf : f.IsDistinguishedAt I) (hf' : f'.IsDistinguishedAt I) :
    (f * f').IsDistinguishedAt I :=
  ⟨hf.toIsWeaklyEisensteinAt.mul hf'.toIsWeaklyEisensteinAt, hf.monic.mul hf'.monic⟩

Похожие утверждения