MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-chr Unicode version

Definition df-chr 16457
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  =  ( g  e.  _V  |->  ( ( od `  g
) `  ( 1r `  g ) ) )

Detailed syntax breakdown of Definition df-chr
StepHypRef Expression
1 cchr 16453 . 2  class chr
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . 5  class  g
5 cur 15339 . . . . 5  class  1r
64, 5cfv 5255 . . . 4  class  ( 1r
`  g )
7 cod 14840 . . . . 5  class  od
84, 7cfv 5255 . . . 4  class  ( od
`  g )
96, 8cfv 5255 . . 3  class  ( ( od `  g ) `
 ( 1r `  g ) )
102, 3, 9cmpt 4077 . 2  class  ( g  e.  _V  |->  ( ( od `  g ) `
 ( 1r `  g ) ) )
111, 10wceq 1623 1  wff chr  =  ( g  e.  _V  |->  ( ( od `  g
) `  ( 1r `  g ) ) )
Colors of variables: wff set class
This definition is referenced by:  chrval  16479
  Copyright terms: Public domain W3C validator