Definition df-chr 21516

Description: The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.)

Assertion

Ref	Expression
df-chr	⊢ chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔)))

Detailed syntax breakdown of Definition df-chr

Step	Hyp	Ref	Expression
1		cchr 21512	. 2 class chr
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4	2	cv 1539	. . . . 5 class 𝑔
5		cur 20178	. . . . 5 class 1r
6	4, 5	cfv 6561	. . . 4 class (1r‘𝑔)
7		cod 19542	. . . . 5 class od
8	4, 7	cfv 6561	. . . 4 class (od‘𝑔)
9	6, 8	cfv 6561	. . 3 class ((od‘𝑔)‘(1r‘𝑔))
10	2, 3, 9	cmpt 5225	. 2 class (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔)))
11	1, 10	wceq 1540	1 wff chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔)))

This definition is referenced by:  chrval  21538