Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-20 19:03 f01c132b

View on Github →

feat(data/sym/basic): combinatorial equivalence for sym (option α) n.succ (#15192) Adds sym_option_succ_equiv.

Estimated changes

Modified src/data/sym/basic.lean

added def sym_option_succ_equiv.decode

added theorem sym_option_succ_equiv.decode_encode

added def sym_option_succ_equiv.encode

added theorem sym_option_succ_equiv.encode_decode

added theorem sym_option_succ_equiv.encode_of_none_mem

added theorem sym_option_succ_equiv.encode_of_not_none_mem

added def sym_option_succ_equiv