Theorem Nat.nth_comp_of_strictMono

Modification history

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