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 | |- chr = ( g e. _V |-> ( ( od ` g ) ` ( 1r ` g ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cchr | |- chr |
|
| 1 | vg | |- g |
|
| 2 | cvv | |- _V |
|
| 3 | cod | |- od |
|
| 4 | 1 | cv | |- g |
| 5 | 4 3 | cfv | |- ( od ` g ) |
| 6 | cur | |- 1r |
|
| 7 | 4 6 | cfv | |- ( 1r ` g ) |
| 8 | 7 5 | cfv | |- ( ( od ` g ) ` ( 1r ` g ) ) |
| 9 | 1 2 8 | cmpt | |- ( g e. _V |-> ( ( od ` g ) ` ( 1r ` g ) ) ) |
| 10 | 0 9 | wceq | |- chr = ( g e. _V |-> ( ( od ` g ) ` ( 1r ` g ) ) ) |