On Sunday, February 6, 2022 at 7:39:19 AM UTC+1 [email protected] wrote:
> ... > This has already appeared in this thread: in AV's code you have ( QFrm ` V > ) as the type of all quadratic forms over V. Or rather it should read that: > there appears to be an error in the code, and the code as written would > have tripped the definition checker. Here's a revised version (still not > checked though): > > Sorry for my mistake, and many thanks to Mario who detected it. It was a little late last night, and I only used metamath.exe to check the definition and the theorems, and not mmj2 which would have detected the mistake by its soundness checks. Of course, the class/vector space V should not be used directly in the definition, but should be made variable by defining QFrm as funktion mapping a set/vector space V to the set of the quadratic forms over this set/vector space. I'll revise my definition and theorems according to Mario's suggestion (at least the distinct variable conditions must be adjusted, and some subtleties with V being a proper class must be considered) in the near future. -- 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/3d17f5e6-1af4-40ee-be77-5d7a48cad8c5n%40googlegroups.com.
