Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tsub_eq_tsub_min

Modification history

2021-10-20 15:39

src/algebra/order/sub.lean

refactor(algebra/order/sub): rename sub -> tsub (#9793) …

Added tsub_eq_tsub_min View on Github →