Commit 2024-03-12 07:55 55524115

View on Github →

chore(Computability): Encodable/Fintype -> Countable/Finite (#10869) Also golf a proof

Estimated changes

Modified Mathlib/Computability/Encoding.lean

modified theorem Computability.Encoding.card_le_aleph0

Modified Mathlib/Computability/Primrec.lean

modified theorem Primrec.dom_fintype

Modified Mathlib/Computability/TuringMachine.lean

modified theorem Turing.TM1to1.exists_enc_dec