Definition df-chr

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)

	Ref	Expression
Assertion	df-chr	$$⊢\mathrm{chr}=\left(g\in \mathrm{V}⟼\mathrm{od}\left(g\right)\left(1_g\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cchr	$$class\mathrm{chr}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		cod	$$class\mathrm{od}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class\mathrm{od}\left(g\right)$$
6		cur	$$class{1}_r$$
7	4 6	cfv	$$class{1}_g$$
8	7 5	cfv	$$class\mathrm{od}\left(g\right)\left(1_g\right)$$
9	1 2 8	cmpt	$$class\left(g\in \mathrm{V}⟼\mathrm{od}\left(g\right)\left(1_g\right)\right)$$
10	0 9	wceq	$$wff\mathrm{chr}=\left(g\in \mathrm{V}⟼\mathrm{od}\left(g\right)\left(1_g\right)\right)$$