Commit 2025-06-07 06:38 4f54a550

chore: better recursor names for ℤ (#25555) Also modify Int.le_induction and Int.le_induction_down to be like Nat.le_induction – induction n, hn using syntax can now be used with the first two recursors. See Zulip.