Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 17:03 69654263

View on Github →

feat(computability/ackermann): the Ackermann function isn't primitive recursive (#15505) See module docs for a thorough explanation of the proof.

Estimated changes

added def ack
added theorem ack_inj_left
added theorem ack_inj_right
added theorem ack_injective_left
added theorem ack_injective_right
added theorem ack_le_ack
added theorem ack_le_iff_left
added theorem ack_le_iff_right
added theorem ack_lt_iff_left
added theorem ack_lt_iff_right
added theorem ack_mkpair_lt
added theorem ack_mono_left
added theorem ack_mono_right
added theorem ack_one
added theorem ack_pos
added theorem ack_strict_mono_left
added theorem ack_strict_mono_right
added theorem ack_succ_succ
added theorem ack_succ_zero
added theorem ack_three
added theorem ack_two
added theorem ack_zero
added theorem add_add_one_le_ack
added theorem add_lt_ack
added theorem lt_ack_left
added theorem lt_ack_right
added theorem max_ack_left
added theorem max_ack_right
added theorem not_primrec_ack_self
added theorem not_primrec₂_ack
added theorem one_lt_ack_succ_left
added theorem one_lt_ack_succ_right