Commit 2024-06-12 08:11 076eee0c

View on Github →

feat: @[simp] Nat.count / Nat.nth of fun _ ↦ True, False (#13378)

Estimated changes

Modified Mathlib/Data/Nat/Count.lean

added theorem Nat.count_false

added theorem Nat.count_of_forall

added theorem Nat.count_of_forall_not

added theorem Nat.count_true

Modified Mathlib/Data/Nat/Nth.lean

added theorem Nat.nth_false

added theorem Nat.nth_of_forall

added theorem Nat.nth_of_forall_not

added theorem Nat.nth_true