### Abstract

Euler's Partition Theorem states that the number of partitions with only distinct parts is equal to the number of partitions with only odd parts. The combinatorial proof follows John Harrison's HOL Light formalization. This theorem is the 45th theorem of the Top 100 Theorems list.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Euler_Partition

- Euler_Partition

### Depends on

- Cardinality of Number Partitions

### Auto-related entries

- Ptolemy’s Theorem
- Pick’s Theorem
- Bertrand’s postulate
- Intersecting Chords Theorem
- Basic Geometric Properties of Triangles

## Cite

×

Euler_Partition-AFP

    @article{Euler_Partition-AFP,
      author  = {Lukas Bulwahn},
      title   = {Euler's Partition Theorem},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Euler_Partition.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Nov 20, 2015 : Isabelle2015