Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_sub'

Modification history

2021-10-25 17:42
src/algebra/order/ring.lean
feat(*): use `ordered_sub` instead of `nat.sub` lemmas (#9855) …
Deleted mul_sub'View on Github →
2021-10-08 07:33
src/algebra/order/ring.lean
feat(algebra/order/ring): variants of mul_sub' (#9604) …
Modified mul_sub'View on Github →
2021-09-15 18:42
src/algebra/ordered_ring.lean
refactor(data/real/nnreal): use `has_ordered_sub` (#9167) …
Added mul_sub'View on Github →