smul_eq_C_smul — Mathlib

English

For x ∈ RatFunc(K) and r ∈ K, the scalar action r • x equals the polynomial-scalar C r acting on x: r • x = C r • x.

Русский

Для x ∈ RatFunc(K) и r ∈ K, скалярное умножение совпадает с умножением на константу: r • x = C r • x.

LaTeX

$$$\forall x\in \mathrm{RatFunc}(K),\; \forall r\in K,\; r \cdot x = \mathrm{C}(r) \cdot x$$$

Lean4

theorem smul_eq_C_smul (x : RatFunc K) (r : K) : r • x = Polynomial.C r • x :=
  by
  obtain ⟨x⟩ := x
  induction x using Localization.induction_on
  rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk, Localization.smul_mk, smul_eq_mul,
    Polynomial.smul_eq_C_mul]

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