Metamath Proof Explorer
Table of Contents - 10.8. The complex numbers as an algebraic extensible structure
- Definition and basic properties
- cpsmet
- cxmet
- cmet
- cbl
- cfbas
- cfg
- cmopn
- cmetu
- df-psmet
- df-xmet
- df-met
- df-bl
- df-mopn
- df-fbas
- df-fg
- df-metu
- ccnfld
- df-cnfld
- cnfldstr
- cnfldex
- cnfldbas
- cnfldadd
- cnfldmul
- cnfldcj
- cnfldtset
- cnfldle
- cnfldds
- cnfldunif
- cnfldfun
- cnfldfunOLD
- cnfldfunALT
- xrsstr
- xrsex
- xrsbas
- xrsadd
- xrsmul
- xrstset
- xrsle
- cncrng
- cnring
- xrsmcmn
- cnfld0
- cnfld1
- cnfldneg
- cnfldplusf
- cnfldsub
- cndrng
- cnflddiv
- cnfldinv
- cnfldmulg
- cnfldexp
- cnsrng
- xrsmgm
- xrsnsgrp
- xrsmgmdifsgrp
- xrs1mnd
- xrs10
- xrs1cmn
- xrge0subm
- xrge0cmn
- xrsds
- xrsdsval
- xrsdsreval
- xrsdsreclblem
- xrsdsreclb
- cnsubmlem
- cnsubglem
- cnsubrglem
- cnsubdrglem
- qsubdrg
- zsubrg
- gzsubrg
- nn0subm
- rege0subm
- absabv
- zsssubrg
- qsssubdrg
- cnsubrg
- cnmgpabl
- cnmgpid
- cnmsubglem
- rpmsubg
- gzrngunitlem
- gzrngunit
- gsumfsum
- regsumfsum
- expmhm
- nn0srg
- rge0srg
- Ring of integers
- czring
- df-zring
- zringcrng
- zringring
- zringabl
- zringgrp
- zringbas
- zringplusg
- zringmulg
- zringmulr
- zring0
- zring1
- zringnzr
- dvdsrzring
- zringlpirlem1
- zringlpirlem2
- zringlpirlem3
- zringinvg
- zringunit
- zringlpir
- zringndrg
- zringcyg
- zringsubgval
- zringmpg
- prmirredlem
- dfprm2
- prmirred
- expghm
- mulgghm2
- mulgrhm
- mulgrhm2
- Algebraic constructions based on the complex numbers
- czrh
- czlm
- cchr
- czn
- df-zrh
- df-zlm
- df-chr
- df-zn
- zrhval
- zrhval2
- zrhmulg
- zrhrhmb
- zrhrhm
- zrh1
- zrh0
- zrhpropd
- zlmval
- zlmlem
- zlmlemOLD
- zlmbas
- zlmbasOLD
- zlmplusg
- zlmplusgOLD
- zlmmulr
- zlmmulrOLD
- zlmsca
- zlmvsca
- zlmlmod
- chrval
- chrcl
- chrid
- chrdvds
- chrcong
- chrnzr
- chrrhm
- domnchr
- znlidl
- zncrng2
- znval
- znle
- znval2
- znbaslem
- znbaslemOLD
- znbas2
- znbas2OLD
- znadd
- znaddOLD
- znmul
- znmulOLD
- znzrh
- znbas
- zncrng
- znzrh2
- znzrhval
- znzrhfo
- zncyg
- zndvds
- zndvds0
- znf1o
- zzngim
- znle2
- znleval
- znleval2
- zntoslem
- zntos
- znhash
- znfi
- znfld
- znidomb
- znchr
- znunit
- znunithash
- znrrg
- cygznlem1
- cygznlem2a
- cygznlem2
- cygznlem3
- cygzn
- cygth
- cyggic
- frgpcyg
- Signs as subgroup of the complex numbers
- cnmsgnsubg
- cnmsgnbas
- cnmsgngrp
- psgnghm
- psgnghm2
- psgninv
- psgnco
- Embedding of permutation signs into a ring
- zrhpsgnmhm
- zrhpsgninv
- evpmss
- psgnevpmb
- psgnodpm
- psgnevpm
- psgnodpmr
- zrhpsgnevpm
- zrhpsgnodpm
- cofipsgn
- zrhpsgnelbas
- zrhcopsgnelbas
- evpmodpmf1o
- pmtrodpm
- psgnfix1
- psgnfix2
- psgndiflemB
- psgndiflemA
- psgndif
- copsgndif
- The ordered field of real numbers
- crefld
- df-refld
- rebase
- remulg
- resubdrg
- resubgval
- replusg
- remulr
- re0g
- re1r
- rele2
- relt
- reds
- redvr
- retos
- refld
- refldcj
- recrng
- regsumsupp
- rzgrp