Decomposition of totally ordered hoops

Sebasti├ín Buss ­čôž

January 22, 2024


We formalize a well known result in theory of hoops: every totally ordered hoop can be written as an ordinal sum of irreducible (equivalently Wajsberg) hoops. This formalization is based on the proof for BL-chains (i.e., bounded totally ordered hoops) found in Decomposition of BL-chains by M. Busaniche (Algebra Universalis, 2005).


BSD License


Session Isabelle_hoops