Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pfun.fix_stop

Modification history

2022-11-10 23:42

src/data/pfun.lean

feat(data/pfun): review APIs, add some lemmas about `fix_induction` (#17004)

Modified pfun.fix_stop View on Github →

2022-03-25 02:56

src/data/pfun.lean

feat(data/pfun): Remove unneeded assumption from pfun.fix_induction (#12920) …

Added pfun.fix_stop View on Github →