Metamath Proof Explorer


Syntax definition cdvh

Description: Extend class notation with constructed full vector space H.

Ref Expression
Assertion cdvh class DVecH