Description: The value of isomorphism H at the lattice unit is the set of all vectors. (Contributed by NM, 13-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dih1.m | |
|
dih1.h | |
||
dih1.i | |
||
dih1.u | |
||
dih1.v | |
||
Assertion | dih1 | |