basic): `order_iso_class` (#12157)

Commit

3 years ago

feat(order/hom/basic): `order_iso_class` (#12157) Define `order_iso_class`, following the hom refactor. Also add a few missing lemmas.

Author

YaelDillies

Parents