Theorem Nat.lt_card_toFinset_of_nth_ne_zero

Modification history

2026-07-17 09:57
Mathlib/Data/Nat/Nth.lean
chore(Data): rename `setOf` to `Set.ofPred` (#41507) …
Modified Nat.lt_card_toFinset_of_nth_ne_zeroView on Github →
2024-11-23 13:41
Mathlib/Data/Nat/Nth.lean
feat(Data/Nat/Nth): `nth p n ≠ 0` lemmas (#19142) …
Added Nat.lt_card_toFinset_of_nth_ne_zeroView on Github →