Description: Define the mapping yielding the basic N -th root of unity. In cxpeq , this is called "the primitive N -th root of unity with the smallest positive argument". (Contributed by AV, 24-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-bru | |- bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cbru | |- bRoU |
|
| 1 | vn | |- n |
|
| 2 | cn | |- NN |
|
| 3 | ce | |- exp |
|
| 4 | c2 | |- 2 |
|
| 5 | cmul | |- x. |
|
| 6 | cpi | |- _pi |
|
| 7 | ci | |- _i |
|
| 8 | 6 7 5 | co | |- ( _pi x. _i ) |
| 9 | 4 8 5 | co | |- ( 2 x. ( _pi x. _i ) ) |
| 10 | cdiv | |- / |
|
| 11 | 1 | cv | |- n |
| 12 | 9 11 10 | co | |- ( ( 2 x. ( _pi x. _i ) ) / n ) |
| 13 | 12 3 | cfv | |- ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) |
| 14 | 1 2 13 | cmpt | |- ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) |
| 15 | 0 14 | wceq | |- bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) |