Description: Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dchrmhm.g | |
|
dchrmhm.z | |
||
dchrmhm.b | |
||
dchrmul.t | |
||
dchrmul.x | |
||
dchrmul.y | |
||
Assertion | dchrmulcl | |