inductionOn vs induction_on

Stream: mathlib4

[Yuyang Zhao]

There are some lemmas named *.inductionOn and some named *.induction_on now, should they be unified? If so, which name should be used?

[Eric Wieser]

Can you give an example of each?

[Ruben Van de Velde]

I think it depends on whether they construct data or not

[Ruben Van de Velde]

Or should

[Yuyang Zhao]

docs4#Quot.inductionOn
docs4#Sym2.inductionOn
docs4#Nat.mod.inductionOn
docs4#Ordinal.inductionOn
These are all theorems (not defs, but there are some elsewhere). Searching in the docs page gives you a lot of examples.

[Yuyang Zhao]

For induction_on:
docs4#Quot.induction_on
docs4#Int.induction_on
docs4#Part.induction_on
docs4#Trunc.induction_on

[Eric Wieser]

Nice catch, especially since some of these are duplicates

[Yuyang Zhao]

inductionOn but defs:
docs4#Vector.inductionOn
docs4#Fin.inductionOn
docs4#Int.inductionOn'

[Ruben Van de Velde]

Should the defs be recOn, though?