Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(algebra/classes): remove redundant assumption from `is_stric…
…t_total_order` (#746) Currently in mathlib, we have the [`is_strict_total_order'`](https://leanprover-community.github.io/mathlib_docs/order/rel_classes.html#is_strict_total_order') class. This is mathematically the same as [`is_strict_total_order`](https://leanprover-community.github.io/mathlib_docs/init/algebra/classes.html#is_strict_total_order), as proven by [`is_strict_total_order_of_is_strict_total_order'`](https://leanprover-community.github.io/mathlib_docs/order/rel_classes.html#is_strict_total_order_of_is_strict_total_order'), but has one assumption less. We remove the redundant assumption from `is_strict_total_order` so that it now exactly matches `is_strict_total_order'`. If this PR is merged, once mathlib is bumped, we'll be left with two identical classes for a short while. There shouldn't be significant breakage, as the unprimed class sees almost no use in `mathlib`. After that, I'll do a separate refactor to remove the redundant typeclass.
- Loading branch information