Commit 2025-07-22 23:07 4b54a1d2

View on Github →

feat(NumberTheory/Divisors): add ne_zero_of_mem_divisors (#27359) Useful for #27358. This PR adds a direct lemma for the fact that a member of the divisor Finset is nonzero.

Estimated changes

Modified Mathlib/NumberTheory/Divisors.lean

modified theorem Nat.dvd_of_mem_divisors

added theorem Nat.ne_zero_of_mem_divisors