| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Euler's Partition Theorem
| Title: | Euler's Partition Theorem |
| Author: | Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com) |
| Submission date: | 2015-11-19 |
| 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. |
| BibTeX: |
@article{Euler_Partition-AFP,
author = {Lukas Bulwahn},
title = {Euler's Partition Theorem},
journal = {Archive of Formal Proofs},
month = nov,
year = 2015,
note = {\url{http://isa-afp.org/entries/Euler_Partition.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Card_Number_Partitions |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |