single_inv — Mathlib

English

Inverse of a monomial corresponds to the monomial with negated exponent and reciprocal coefficient.

Русский

Обратная монома соответствует моному с отрицательным показателем степени и обратным коэффициентом.

LaTeX

$$$\text{if } h\neq 0,\; \mathrm{single}(-d)(\alpha)^-1 = (\mathrm{single}(d)(\alpha))^{-1}$$$

Lean4

theorem single_inv (d : ℤ) {α : F} (hα : α ≠ 0) : single (-d) (α⁻¹ : F) = (single (d : ℤ) (α : F))⁻¹ :=
  by
  apply eq_inv_of_mul_eq_one_right
  simp [hα]

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