Adding fin.induction_zero and induction_succ lemmas

Stream: maths

[Diana Kalinichenko]

Hi! I'd like to add fin.induction_zero and fin.induction_succ lemmas, similar to fin.cases_zero and fin.cases_succ, to data.fin.basic. My pull request is here: https://github.com/leanprover-community/mathlib/pull/15057. Please grant me access to non-master branches of repository :)

[Kevin Buzzard]

Diana the workflow here is that for CI reasons we only look at PRs made from non-master branches; you seem to be aware of this :-) @maintainers Diana's github userid seems to be technosentience. Diana after you have access can you push to a branch, open a new PR from the branch and then close #15057 ?

[Diana Kalinichenko]

Yeah, I've realised that only after I made the PR. :sweat_smile: I'll do that right after I have access.

[Markus Himmel]

@Diana Kalinichenko I sent you an invitation: https://github.com/leanprover-community/mathlib/invitations

[Diana Kalinichenko]

Done, I've re-created the pull request.