Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drngui.b | |
|
drngui.z | |
||
drngui.r | |
||
Assertion | drngui | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngui.b | |
|
2 | drngui.z | |
|
3 | drngui.r | |
|
4 | eqid | |
|
5 | 1 4 2 | isdrng | |
6 | 3 5 | mpbi | |
7 | 6 | simpri | |
8 | 7 | eqcomi | |