Commit 2025-09-02 04:47 36bfae37

View on Github →

chore(Nat/Prime/Basic): ne_zero instead of pos hypothesis (#28921) There are some lean core lemmas that are of the 0 < x form that lemmas here relied on. That is why they were in the same hypothesis shape. We prefer the weaker hypothesis.

Estimated changes

Modified Mathlib/Data/Nat/Prime/Basic.lean

modified theorem Nat.coprime_of_lt_prime

modified theorem Nat.eq_or_coprime_of_le_prime

Modified Mathlib/Data/Nat/Totient.lean

modified theorem Nat.Ico_filter_coprime_le

Modified Mathlib/NumberTheory/PrimeCounting.lean

modified theorem Nat.primeCounting'_add_le