Definition df-bru 49738

Description: Define the mapping yielding the basic 𝑁-th root of unity. In cxpeq 27131, this is called "the primitive 𝑁-th root of unity with the smallest positive argument". (Contributed by AV, 24-Oct-2026.)

Assertion

Ref	Expression
df-bru	⊢ bRoU = (𝑛 ∈ ℕ ↦ (exp‘((2 · (π · i)) / 𝑛)))

Detailed syntax breakdown of Definition df-bru

Step	Hyp	Ref	Expression
1		cbru 49737	. 2 class bRoU
2		vn	. . 3 setvar 𝑛
3		cn 12373	. . 3 class ℕ
4		c2 12435	. . . . . 6 class 2
5		cpi 16273	. . . . . . 7 class π
6		ci 11239	. . . . . . 7 class i
7		cmul 11242	. . . . . . 7 class ·
8	5, 6, 7	co 7449	. . . . . 6 class (π · i)
9	4, 8, 7	co 7449	. . . . 5 class (2 · (π · i))
10	2	cv 1569	. . . . 5 class 𝑛
11		cdiv 12011	. . . . 5 class /
12	9, 10, 11	co 7449	. . . 4 class ((2 · (π · i)) / 𝑛)
13		ce 16268	. . . 4 class exp
14	12, 13	cfv 6564	. . 3 class (exp‘((2 · (π · i)) / 𝑛))
15	2, 3, 14	cmpt 5190	. 2 class (𝑛 ∈ ℕ ↦ (exp‘((2 · (π · i)) / 𝑛)))
16	1, 15	wceq 1570	1 wff bRoU = (𝑛 ∈ ℕ ↦ (exp‘((2 · (π · i)) / 𝑛)))

This definition is used by:  bruval  49739