Decomposition of totally ordered hoops

Sebastián Buss 📧

January 22, 2024

Abstract

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).

License

BSD License

Topics

Session Isabelle_hoops

Cite

× 
@article{Isabelle_hoops-AFP,
  author  = {Sebastián Buss},
  title   = {Decomposition of totally ordered hoops},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Isabelle_hoops.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest