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	⊢ bRoU = ( 𝑛 ∈ ℕ ↦ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbru	⊢ bRoU
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		ce	⊢ exp
4		c2	⊢ 2
5		cmul	⊢ ·
6		cpi	⊢ π
7		ci	⊢ i
8	6 7 5	co	⊢ ( π · i )
9	4 8 5	co	⊢ ( 2 · ( π · i ) )
10		cdiv	⊢ /
11	1	cv	⊢ 𝑛
12	9 11 10	co	⊢ ( ( 2 · ( π · i ) ) / 𝑛 )
13	12 3	cfv	⊢ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) )
14	1 2 13	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) ) )
15	0 14	wceq	⊢ bRoU = ( 𝑛 ∈ ℕ ↦ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) ) )