Theorem Int.leInductionDown_sub_one

Modification history

2026-05-10 01:42
Mathlib/Data/Int/Init.lean
chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas (#37171) …
Added Int.leInductionDown_sub_oneView on Github →