Zulip Chat Archive
Stream: Is there code for X?
Topic: Nat.sub_le_sub
David E. Narváez (Feb 28 2025 at 15:04):
Is there really no Nat version of https://leanprover-community.github.io/mathlib4_docs/Init/Data/Int/Order.html#Int.sub_le_sub
Yaël Dillies (Feb 28 2025 at 15:04):
David E. Narváez (Feb 28 2025 at 15:11):
Ah, great, thanks!
Weiyi Wang (Mar 02 2025 at 02:41):
TIL t stands for truncated. I have been calling it saturated sub, coming from other programming languages
Last updated: May 02 2025 at 03:31 UTC