help with characteristic of rings

Stream: general

[Scott Morrison]

Can someone point me to the fact that if a field k has characteristic p and p does not divide n : nat, then (n : k) is nonzero?

[Yury G. Kudryashov]

char_p.cast_eq_zero_iff?

[Yury G. Kudryashov]

It's in the definition of class char_p.

[Scott Morrison]

oh

[Scott Morrison]

:-)

[Scott Morrison]

thanks