Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dchrmhm.g | |
|
dchrmhm.z | |
||
dchrmhm.b | |
||
dchrn0.b | |
||
dchrn0.u | |
||
dchr1cl.o | |
||
dchrmulid2.t | |
||
dchrmulid2.x | |
||
dchrinvcl.n | |
||
Assertion | dchrinvcl | |