### 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

- Mathematics/Algebra

### Session Isabelle_hoops

- Posets
- Hoops
- Ordinal_Sums
- Totally_Ordered_Hoops
- BL_Chains

## Cite

×

Isabelle_hoops-AFP

    @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