Hi, folks,
I am a newbie and I have a question about expressing a quadratic form over
a vector space.
Just follow cases in set.mm, I give below definition of a quadratic form
```metamath
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Quadratic Form
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
A quadratic form over a field K is
a map q: V -> K from a finite-dimensional K-vector space to K
such that q(av) = a^2 q(v) for all a \in K, v \in V.
$)
$c QFrm $.
$( Extend class notation with class of all quadratic forms. $)
cqfrm $a class QFrm $.
df-qfrm $a |- QFrm = { V --> ( Scalar ` V ) | V e. LVec /\
q e. V --> ( Scalar ` V ) /\ v e. V /\ a e. ( Scalar ` V ) /\
q ` ( a .x. v ) = ( a * a ) .x. v }
$.
```
But I found it is difficult to express special quadratic forms over R^3
In Haskell or similar languages which support algebraic data types, we can
define
```haskell
data Tree a = Tip | Node (Tree a) a (Tree a)
```
Here a is a type parameter.
So my questions are:
(1) Is the definition of Quadratic Form correct?
(2) How can we express something like a type with parameter and the
initialization of a type with parameter.
Thanks a lot.
Mingli
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAGDRuAg4F%3Deb2qSTLBsXwX7yz05W7b6PBR%2BX%2B2Q-zCBB7E6RbA%40mail.gmail.com.
