smul — Mathlib

English

If f is Weierstrass division at g with q and r over I, then a scalar multiple a•f is Weierstrass division at g with a•q and a•r.

Русский

Если f — деление Вайершстраса, то a•f — тоже деление с a•q и a•r.

LaTeX

$$$\\forall {A} [\\text{CommRing } A], \\; (f IsWeierstrassDivisionAt g q r I) \\Rightarrow \\forall a \\in A, (a \\cdot f).IsWeierstrassDivisionAt g (a \\cdot q) (a \\cdot r) I$$$

Lean4

theorem smul (H : f.IsWeierstrassDivisionAt g q r I) (a : A) : (a • f).IsWeierstrassDivisionAt g (a • q) (a • r) I :=
  ⟨(Polynomial.degree_smul_le a _).trans_lt H.degree_lt, by
    simp [H.eq_mul_add, Algebra.smul_def, mul_add, mul_left_comm]⟩

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