Theorem Nat.strong_decreasing_induction

Modification history

2024-05-22 13:33
Mathlib/Data/Nat/Interval.lean
feat(Mathlib.Algebra.Polynomial.RingDivision): add Polynomial.nmem_nonZeroDivisors_iff (#12950) …
Added Nat.strong_decreasing_inductionView on Github →