*): drop some `[nontrivial _]` assumptions (#10550)

Commit

4 years ago

chore(algebra/order/*): drop some `[nontrivial _]` assumptions (#10550) Use `pullback_nonzero` to deduce `nontrivial _` in some `function.injective.*` constructors.

Author

urkud

Parents

0f12400c

mathlib 70435215 - chore(algebra/order/*): drop some `[nontrivial _]` assumptions (#10550)

mathlib
70435215 - chore(algebra/order/*): drop some `[nontrivial _]` assumptions (#10550)