The ring of complex numbers

Content created by Louis Wasserman.

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

module complex-numbers.ring-of-complex-numbers where
Imports 
open import commutative-algebra.commutative-rings

open import complex-numbers.additive-group-of-complex-numbers
open import complex-numbers.complex-numbers
open import complex-numbers.multiplication-complex-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.universe-levels

open import ring-theory.rings

Idea

The type of complex numbers equipped with multiplication and addition is a commutative ring.

Definition

ring-ℂ-lzero : Ring (lsuc lzero)
ring-ℂ-lzero =
  ( ab-add-ℂ-lzero ,
    ( mul-ℂ , associative-mul-ℂ) ,
    ( one-ℂ , left-unit-law-mul-ℂ , right-unit-law-mul-ℂ) ,
    left-distributive-mul-add-ℂ ,
    right-distributive-mul-add-ℂ)

commutative-ring-ℂ-lzero : Commutative-Ring (lsuc lzero)
commutative-ring-ℂ-lzero =
  ( ring-ℂ-lzero ,
    commutative-mul-ℂ)

Recent changes