Zulip Chat Archive

Stream: mathlib4

Topic: change name of `Int.le_induction_down`

Yi.Yuan (Mar 07 2025 at 08:43):

There are two similar theorems (Int.le_induction_down) and (Nat.decreasingInduction'). These two having different names is not normal. Should we change the name?

Kim Morrison (Mar 20 2025 at 23:13):

Sure! Do you have a suggestion for making these uniform? @Yi.Yuan

Last updated: May 02 2025 at 03:31 UTC