Theorem tsub_tsub_eq_add_tsub_of_le

Modification history

2024-07-31 23:15
Mathlib/Algebra/Order/Sub/Canonical.lean
chore: backports for leanprover/lean4#4814 (part 6) (#15313) …
Modified tsub_tsub_eq_add_tsub_of_leView on Github →
2023-12-04 22:16
Mathlib/Algebra/Order/Sub/Canonical.lean
feat(Algebra/Order/Sub/Canonical): add `tsub_tsub_eq_add_tsub_of_le` (#8804)
Added tsub_tsub_eq_add_tsub_of_leView on Github →