instNeg — Mathlib

English

The ArchimedeanClass is equipped with a negation operation defined by x ↦ x⁻¹, with compatibility ensuring mk(x⁻¹) = - mk(x).

Русский

ArchimedeanClass снабжён операцией отрицания, заданной отображением x ↦ x⁻¹, причем mk(x⁻¹) = -mk(x).

LaTeX

$$$\operatorname{mk}(x^{-1}) = -\operatorname{mk}(x).$$$

Lean4

instance : Neg (ArchimedeanClass R) where
  neg :=
    lift (fun x ↦ mk x⁻¹) fun x y h ↦ by
      have := IsOrderedRing.toIsStrictOrderedRing R
      obtain rfl | hx := eq_or_ne x 0
      · simp_all
      obtain rfl | hy := eq_or_ne y 0
      · simp_all
      have hx' : mk x ≠ ⊤ := by simpa using hx
      apply add_left_cancel_of_ne_top hx'
      nth_rw 2 [h]
      simp [← mk_mul, hx, hy]

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