Extensionality of multiplication of real numbers as a bilinear form

Content created by Louis Wasserman.

Created on 2025-11-26.
Last modified on 2025-11-26.

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

module real-numbers.extensionality-multiplication-bilinear-form-real-numbers where
Imports 
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.absolute-value-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.raising-universe-levels-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.square-roots-nonnegative-real-numbers
open import real-numbers.squares-real-numbers

Idea

If the square of a real number is similar to 0, the real number is similar to 0. This property is extensionality of multiplication as a bilinear form over the real vector space of real numbers.

Proof

abstract
  sim-zero-sim-zero-square-ℝ :
    {l : Level} (x : ℝ l) → sim-ℝ (square-ℝ x) zero-ℝ → sim-ℝ x zero-ℝ
  sim-zero-sim-zero-square-ℝ x x²~0 =
    sim-zero-sim-zero-abs-ℝ
      ( x)
      ( inv-tr
        ( λ y → sim-ℝ y zero-ℝ)
        ( eq-abs-sqrt-square-ℝ x)
        ( transitive-sim-ℝ _ _ _
          ( sim-eq-ℝ real-sqrt-zero-ℝ⁰⁺)
          ( preserves-sim-sqrt-ℝ⁰⁺
            ( nonnegative-square-ℝ x)
            ( zero-ℝ⁰⁺)
            ( x²~0))))

  eq-zero-eq-zero-square-ℝ :
    {l : Level} (x : ℝ l) → square-ℝ x ＝ raise-ℝ l zero-ℝ →
    x ＝ raise-ℝ l zero-ℝ
  eq-zero-eq-zero-square-ℝ {l} x x²=0 =
    eq-sim-ℝ
      ( transitive-sim-ℝ _ _ _
        ( sim-raise-ℝ l zero-ℝ)
        ( sim-zero-sim-zero-square-ℝ
          ( x)
          ( transitive-sim-ℝ _ _ _ (sim-raise-ℝ' l zero-ℝ) (sim-eq-ℝ x²=0))))

Recent changes