nnqsmul_eq_C_mul — Mathlib

English

For a DivisionSemiring R and a nonnegative rational q, the natural nonnegative rational scalar action on polynomials satisfies q • f = C(q) · f.

Русский

Для кольца с делением R и неотрицательного рационального числа q скалярное умножение на q действует на полиномы так: q • f = C(q) · f.

LaTeX

$$q • f = C(q) · f$$

Lean4

theorem nnqsmul_eq_C_mul (q : ℚ≥0) (f : R[X]) : q • f = Polynomial.C (q : R) * f := by
  rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

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