Theorem Nat.nth_mem_of_ne_zero

Modification history

2024-11-23 13:41
Mathlib/Data/Nat/Nth.lean
feat(Data/Nat/Nth): `nth p n ≠ 0` lemmas (#19142) …
Added Nat.nth_mem_of_ne_zeroView on Github →