Definition df-bru

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	Could not format assertion : No typesetting found for |- bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbru	Could not format bRoU : No typesetting found for class bRoU with typecode class
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		ce	$$class\exp$$
4		c2	$$class2$$
5		cmul	$$class\times$$
6		cpi	$$class\mathrm{\pi }$$
7		ci	$$class\mathrm{i}$$
8	6 7 5	co	$$class\mathrm{\pi }\mathrm{i}$$
9	4 8 5	co	$$class2\mathrm{\pi }\mathrm{i}$$
10		cdiv	$$class÷$$
11	1	cv	$$setvarn$$
12	9 11 10	co	$$class\left(\frac{2\mathrm{\pi }\mathrm{i}}{n}\right)$$
13	12 3	cfv	$$class{\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{n}}$$
14	1 2 13	cmpt	$$class\left(n\in \mathbb{N}⟼{\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{n}}\right)$$
15	0 14	wceq	Could not format bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) : No typesetting found for wff bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) with typecode wff