single_div_single — Mathlib

English

Dividing two single terms produces a single term whose exponent is the difference of exponents and whose coefficient is the ratio of coefficients.

Русский

Деление двух одночленных выражений дает одночлен с показателем степени, равным разности степеней, и коэффициентом, равным отношению коэффициентов.

LaTeX

$$ single a r / single b s = single (a - b) (r / s) $$

Lean4

@[simp]
theorem single_div_single (a b : Γ) (r s : R) : single a r / single b s = single (a - b) (r / s) := by
  rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]

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