num_div_dvd' — Mathlib

English

For any RatFunc x, the fraction num(x) / denom(x) equals x.

Русский

Для любой рациональной функции x дробь num(x)/denom(x) равна x.

LaTeX

$$$\dfrac{\operatorname{num}(x)}{\operatorname{denom}(x)} = x$$$

Lean4

/-- A version of `num_div_dvd` with the LHS in simp normal form -/
@[simp]
theorem num_div_dvd' (p : K[X]) {q : K[X]} (hq : q ≠ 0) : C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p := by
  simpa using num_div_dvd p hq

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