Commit 2025-07-30 21:33 6584aff6

View on Github →

chore(Nat): change argument from 0 < n to n ≠ 0 (#27647) Style guide says arguments should be in the weaker form Some proofs got longer because internally they had 0 < n available or relied on iffs that simplified statements about positive elements

Estimated changes

added theorem Nat.choose_ne_zero
added theorem Nat.choose_ne_zero_iff
modified theorem Nat.maxPowDiv.le_of_dvd
modified theorem nat_log_eq_padicValNat_iff
modified theorem one_le_padicValNat_of_dvd
modified theorem padicValNat_def'
modified theorem padicValNat_def