Commit 2021-12-06 13:54 05445629

View on Github →

chore: small progress on equiv and list basics (#124)

  • small progress on equiv and list basics
  • Apply suggestions from code review
  • removing @[simp] from theorem
  • adapting names and filling another gap in Logic.Function.Basic
  • fixing lint
  • fixing functor and removing simp mark
  • recovering commented theorem marked with simp
  • removing theorem without simp mark
  • adding old todo theorem

Estimated changes

added theorem Equiv.apply_symm_apply
added theorem Equiv.coe_fn_mk
added theorem Equiv.inv_fun_as_coe
added def Equiv.perm
added def Equiv.refl
added theorem Equiv.self_comp_symm
added def Equiv.symm
added theorem Equiv.symm_apply_apply
added theorem Equiv.symm_comp_self
added theorem Equiv.to_fun_as_coe
added def Equiv.trans
added structure Equiv
deleted theorem equiv.apply_symm_apply
deleted theorem equiv.coe_fn_mk
deleted def equiv.perm
deleted def equiv.refl
deleted theorem equiv.self_comp_symm
deleted def equiv.symm
deleted theorem equiv.symm_apply_apply
deleted theorem equiv.symm_comp_self
deleted def equiv.trans
deleted structure equiv
deleted theorem List.repeatSucc
added theorem List.repeat_succ