Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-13 17:31 da13598d

View on Github →

feat(model_theory/encoding): Bundled encoding of terms (#13226) Bundles term.list_encode and term.list_decode into a computability.encoding

Estimated changes

Modified src/model_theory/encoding.lean

modified theorem first_order.language.term.card_le

modified def first_order.language.term.list_encode

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.mk_list_eq_max_mk_omega