Commit 2024-04-24 14:51 8656fa6a

View on Github →

chore(Perm/List): golf, review API (#12302)

  • add mem_or_mem_of_zipWith_swap_prod_ne, a version of zipWith_swap_prod_support' without any Finsets;
  • move it and related lemmas up, use them to golf lemmas about formPerm;
  • convert explicit -> implicit arguments here and there;
  • formPerm_reverse doesn't need Nodup

Estimated changes

modified theorem List.formPerm_reverse