mathlib3

e7425e7b - feat(data/fin/basic): `induction_zero` and `induction_succ` lemmas (#15060)

feat(data/fin/basic): `induction_zero` and `induction_succ` lemmas (#15060) This pull request introduces `fin.induction_zero` and `fin.induction_succ` simp lemmas for `fin.induction`, similar to `fin.cases_zero` and `fin.cases_succ` for `fin.cases`.