Theorem Int.inductionOn'_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) …
Modified Int.inductionOn'_sub_oneView on Github →
2024-06-12 08:11
Mathlib/Data/Int/Defs.lean
feat(Algebra): auxiliary results for proofs about elliptic divisibility sequences (#13153) …
Added Int.inductionOn'_sub_oneView on Github →