div_smul — Mathlib

English

For a scalar c and polynomials p,q, the map distributes over division: algebraMap(c·p)/algebraMap(q) equals c·(algebraMap(p)/algebraMap(q)).

Русский

Для скаляра c и многочленов p,q распределение по умножению в числителе и знаменателе: a(c·p)/a(q) = c·(a(p)/a(q)).

LaTeX

$$$\\frac{\\phi(c)\\,\\phi(p)}{\\phi(q)} = \\phi(c) \\cdot \\frac{\\phi(p)}{\\phi(q)}$$$

Lean4

@[simp]
theorem div_smul {R} [Monoid R] [DistribMulAction R K[X]] [IsScalarTower R K[X] K[X]] (c : R) (p q : K[X]) :
    algebraMap _ (RatFunc K) (c • p) / algebraMap _ _ q = c • (algebraMap _ _ p / algebraMap _ _ q) := by
  rw [← mk_eq_div, mk_smul, mk_eq_div]

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