Jun Xu (Jan 24 2026 at 09:29): Jun Xu (Jan 24 2026 at 09:29):Is there a widely accepted implementation of finite Cartesian products for structures such as groups, rings and lattices?
I recently encountered a problem where I have to implement the said construct, but found no library to my satisfaction. The present solutions seem to be:
1) A DIY list-based implementation
2) https://www.isa-afp.org/browser_info/current/HOL/HOL-Analysis/Finite_Cartesian_Product.html, which works on a type level.
I went for 1, because 2 works at the type level, but I need something with terms (for example, https://isabelle.in.tum.de/library/HOL/HOL-Algebra/outline.pdf).
Is it true that whenever you need products you just have to write a library yourself?
Last updated: Feb 06 2026 at 20:37 UTC