Characteristic of a field is > n

Stream: Is there code for X?

[Stepan Nesterov]

I would like to formally state the following theorem:
If $K$ is a field, and $G$ is a group, if $U$ and $V$ are two representations of $G$, if $K$ is of characteristic zero, or $\mathrm{char} K > \dim U, \dim V$, then if for any $g \in G$, the trace of $g$ on $U$ is the same as the trace of $g$ on $V$, then $U$ and $V$ are equivalent.

What is a good way to spell an assumption on the characteristic? What I really want is that the restriction of ‘natCast’ to ‘Fin n’ is injective. I could either say this directly or opt for an assumption of the form ‘CharZero K \or n < ringChar K’. Both of these options feel a bit clunky to me. Is there a better way?

[Kevin Buzzard]

You could just use the assertion that you'll use in the proof, namely that $n!$ is invertible in $K$, where $n$ runs through the dimensions.