polynomial — Mathlib

English

If an element a is IsSMulRegular on R, then it is IsSMulRegular on the polynomial ring R[X].

Русский

Если элемент a обладает свойством IsSMulRegular на R, то он обладает тем же свойством на кольце полиномов R[X].

LaTeX

$$$\\operatorname{IsSMulRegular}(R, a) \\Rightarrow \\operatorname{IsSMulRegular}(R[X], a)$$$

Lean4

theorem _root_.IsSMulRegular.polynomial {S : Type*} [SMulZeroClass S R] {a : S} (ha : IsSMulRegular R a) :
    IsSMulRegular R[X] a
  | ⟨_x⟩, ⟨_y⟩, h => congr_arg _ <| ha.finsupp (Polynomial.ofFinsupp.inj h)

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