Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-04 15:08 b7d314f3

View on Github →

feat(tactic/tfae): tactic for decomposing a proof into a set of equivalent propositions which can be proved equivalent by cyclical implications

Estimated changes

added def list.mmap_accuml
added def list.mmap_accumr
added def list.last'
added theorem list.last'_mem
added theorem list.tfae.out
added def list.tfae
added theorem list.tfae_cons_cons
added theorem list.tfae_cons_of_mem
added theorem list.tfae_nil
added theorem list.tfae_of_cycle
added theorem list.tfae_singleton
added inductive tactic.tfae.arrow