inv_single — Mathlib

English

The inverse of a single term is the corresponding negative index with reciprocal coefficient: (single a r)^{-1} = single (-a) r^{-1}.

Русский

Обратный элемент однородного члена: (single a r)^{-1} = single (-a) r^{-1}.

LaTeX

$$ (single a r)^{-1} = single (-a) r^{-1} $$

Lean4

@[simp]
theorem inv_single (a : Γ) (r : R) : (single a r)⁻¹ = single (-a) r⁻¹ :=
  by
  obtain rfl | hr := eq_or_ne r 0
  · simp [inv_def]
  · simp [inv_def, hr]

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