Commit 2021-02-26 00:42 27559398
View on Github →feat(data/pnat/basic): add induction principle (#6410)
An induction principle for pnat. The proof is by Mario Carneiro. If there are mistakes, I introduced them!
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/torsion.20free/near/227748865