Metamath Proof Explorer
Table of Contents - 20.3.14.3. Canonical embedding of the field of the rational numbers into a division ring
- cqqh
- df-qqh
- qqhval
- zrhf1ker
- zrhchr
- zrhker
- zrhunitpreima
- elzrhunit
- elzdif0
- qqhval2lem
- qqhval2
- qqhvval
- qqh0
- qqh1
- qqhf
- qqhvq
- qqhghm
- qqhrhm
- qqhnm
- qqhcn
- qqhucn