Thanks, Alex and vvs Quadratic form is widely used, but looks like it is still missing in metamath. I guess I need the bilinear condition but I'm not sure about it. In fact, following paper[1], I am trying to solve Pascal's Hexagon theorem.
If not wrong, I did not see too many obstacles for the formalization of the simple proof. The next step is to introduce homogeneous coordinates which connect conic sections in 2d with quadratic form in 3d. And then by some algebraic property of cross product in 3d space to prove the theorem. (we still do not have cross product in 3d?) Maybe difficult for a newbie to solve, at least it is a good chance for exercises. So far the learning curve is a little bit steep because a lot of conventions are not documented? But the community is very nice, which reminds me of Norm. [1]: A very simple proof of Pascal’s hexagon theorem and some applications by Nedeljko Stefanovic and Milos Milosevic On Sun, Feb 6, 2022 at 7:10 AM vvs <[email protected]> wrote: > Hi Mingli, > > (2) How can we express something like a type with parameter and the >> initialization of a type with parameter. >> > > I'm not an expert, so don't take my word for it. But let me guess. Haskell > is based on simple type theory while set.mm is ZFC, i.e. set theory. They > are different beasts. You can embed type theory, of course, but that would > not be set.mm anymore, IMHO. > > But maybe some real expert will say that I'm telling nonsensicality and > this should be easy to do :) > > -- > 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/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4bef40e5-3ab7-402d-850c-e08aaeb0edcan%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAGDRuAhT3ZADrOrPF3%3D9nVv3SZCVj8ZVh5_Rv%3D%2BRZMErfqvHYQ%40mail.gmail.com.
