Commit 2025-09-16 10:17 cd010f0c

View on Github →

feat: grind annotations for Nat.count (#29454)

Estimated changes

Modified Mathlib/Algebra/Group/Embedding.lean

Modified Mathlib/Data/Nat/Count.lean

modified theorem Nat.count_lt_count_succ_iff

modified theorem Nat.count_succ_eq_count_iff

modified theorem Nat.count_succ_eq_succ_count_iff

modified theorem Nat.count_zero