Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-01 03:45 5c278857

View on Github →

feat(order/order_iso): group structure on order automorphisms (#2875) Also add a few missing lemmas about order_iso

Estimated changes

modified theorem order_iso.apply_symm_apply
modified theorem order_iso.coe_fn_injective
added theorem order_iso.coe_mul
added theorem order_iso.coe_one
added theorem order_iso.ext
added theorem order_iso.mul_apply
deleted def order_iso.preimage
added def order_iso.rsymm
modified theorem order_iso.symm_apply_apply
deleted theorem order_iso.to_equiv_to_fun
modified theorem order_iso.trans_apply