Theorem Int.leInductionDown_base

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_baseView on Github →