theorem
proved
PRCCharacterPrimeIdentityBranchUniform_of_trace_coherence
show as:
PRCCharacterPrimeIdentityBranchUniform_of_trace_coherence