theorem :: HERMITAN:67

for V being VectSp of F_Complex
for f being diagReR+0valued hermitan-Form of V holds rightker (ScalarForm f) = rightker (Q*Form f) by Th56;