`of_dual` (#13788)

Commit

3 years ago

feat(order/*): Order constructions under `to_dual`/`of_dual` (#13788) A few missing lemmas about `of_dual` and `to_dual`.

Author

YaelDillies

Parents