induction on fin

Stream: general

[Albert ten Napel]

I see a nice definition of fin in terms of a structure here: https://github.com/leanprover/lean/blob/master/library/init/data/fin/basic.lean . But where is induction on this fin defined?

[Rob Lewis]

Are you looking for docs#fin.succ_rec ?

[Albert ten Napel]

Exactly, thanks!