Email Gateway (Aug 22 2022 at 09:15): Email Gateway (Aug 22 2022 at 09:15):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
recently I started to formalize linear algebra results based on HOL-Algebra (Matrices, Determinants, Eigenvalues, Gauss-Jordan-Elimination, …)
while doing this I noticed a annoying difference between setprod and finprod (or setsum and finsum):
the set-based variants define the sum or product of an infinite set as the neutral element, whereas finsum and finprod take „undefined“.
To have more similarity between the two operators I propose to change the definition of finprod from „undefined“ to 1 (which entails 0 for finsum).
Then a lot of lemmas for finprod and finsum can be simplified where often the assumption „finite A“ is now obsolete (and they more closely relate to corresponding setprod and setsum lemmas).
If this change is appreciated, then can someone please include the following patch?
It adapts all of HOL/Algebra to the change and also those entries of the AFP which rely on HOL-Algebra still compile
(Free-Groups Jordan_Hoelder Koenigsberg_Friendship Lehmer Matrix Perfect-Number-Thm Secondary_Sylow Tarskis_Geometry VectorSpace)
I tested everything with Isabelle 8614f8f0fb4b and AFP 7c57eabaad4b.
Best regards,
René
finprod.patch
Last updated: Apr 26 2024 at 01:06 UTC