ofMul_inv — Mathlib

English

If α has an inverse operation, then the additive image of the multiplicative inverse equals the negation of the additive image: ofMul(x^{-1}) = − ofMul(x).

Русский

Пусть у α есть операция обращения; тогда образ x^{-1} в аддитивной копии равен отрицанию образа x: ofMul(x^{-1}) = − ofMul(x).

LaTeX

$$ofMul(x^{-1}) = -\,ofMul(x)$$

Lean4

@[simp]
theorem ofMul_inv [Inv α] (x : α) : ofMul x⁻¹ = -ofMul x :=
  rfl

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