Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-20 03:28 bfe9c6c1

View on Github →

chore(data/pfun): run #sanity_check (#1463)

Estimated changes

added theorem pfun.ext'
deleted def pfun.ext'
added theorem pfun.ext
deleted def pfun.ext
deleted theorem pfun.fix_induction
added theorem pfun.mem_preimage
deleted def pfun.mem_preimage
added theorem roption.ext'
deleted def roption.ext'
added theorem roption.ext
deleted def roption.ext