mathlib3

ef24aced - feat(order/hom/basic): some lemmas about order homs and equivs (#14872)

feat(order/hom/basic): some lemmas about order homs and equivs (#14872) A few lemmas from #11053, which I have seperated from the original PR following @riccardobrasca's suggestion. Co-authored-by: Eric Weiser <wieser.eric@gmail.com>