inv_neg — Mathlib

English

Negation commutes with inversion: (-a)^{-1} = - a^{-1} for all a ∈ EReal.

Русский

Отрицание коммутирует с инверсией: (-a)^{-1} = - a^{-1} для всех a ∈ EReal.

LaTeX

$$$ (-a)^{-1} = -a^{-1} \quad (a \in \mathrm{EReal}) $$$

Lean4

theorem inv_neg (a : EReal) : (-a)⁻¹ = -a⁻¹ := by
  induction a
  · rw [neg_bot, inv_top, inv_bot, neg_zero]
  · rw [← coe_inv _, ← coe_neg _⁻¹, ← coe_neg _, ← coe_inv (-_)]
    exact EReal.coe_eq_coe_iff.2 _root_.inv_neg
  · rw [neg_top, inv_bot, inv_top, neg_zero]

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