Multiplicative inverses of negative real numbers

Content created by Louis Wasserman.

Created on 2025-10-15.
Last modified on 2025-10-15.

{-# OPTIONS --lossy-unification #-}

module real-numbers.multiplicative-inverses-negative-real-numbers where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.multiplication-real-numbers
open import real-numbers.multiplicative-inverses-positive-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.negative-real-numbers
open import real-numbers.positive-and-negative-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers

Idea

If a real number x is negative, then it has a multiplicative inverse, a unique, negative real number y such that the product of x and y is 1.

Definition

inv-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ⁻ l
inv-ℝ⁻ x = neg-ℝ⁺ (inv-ℝ⁺ (neg-ℝ⁻ x))

real-inv-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ l
real-inv-ℝ⁻ x = real-ℝ⁻ (inv-ℝ⁻ x)

Properties

The multiplicative inverse is a multiplicative inverse

abstract
  left-inverse-law-mul-ℝ⁻ :
    {l : Level} (x : ℝ⁻ l) → sim-ℝ (real-inv-ℝ⁻ x *ℝ real-ℝ⁻ x) one-ℝ
  left-inverse-law-mul-ℝ⁻ x⁻@(x , _) =
    inv-tr
      ( λ y → sim-ℝ y one-ℝ)
      ( left-negative-law-mul-ℝ _ _ ∙ inv (right-negative-law-mul-ℝ _ _))
      ( left-inverse-law-mul-ℝ⁺ (neg-ℝ⁻ x⁻))

  right-inverse-law-mul-ℝ⁻ :
    {l : Level} (x : ℝ⁻ l) → sim-ℝ (real-ℝ⁻ x *ℝ real-inv-ℝ⁻ x) one-ℝ
  right-inverse-law-mul-ℝ⁻ x =
    tr
      ( λ y → sim-ℝ y one-ℝ)
      ( commutative-mul-ℝ _ _)
      ( left-inverse-law-mul-ℝ⁻ x)

Recent changes