Theorem Nat.nth_add_one_eq_sub

Modification history

2024-12-20 13:13
Mathlib/Data/Nat/Nth.lean
feat(Data/Nat/Nth): `nth_add_one` (#18836) …
Added Nat.nth_add_one_eq_subView on Github →