Commit 2025-03-08 12:16 b1a6dd97

View on Github →

chore: move the group of relation automorphisms under Algebra.Order (#22505) Order.RelIso.Group imports algebra, hence should be under Algebra

Estimated changes

added theorem RelIso.apply_eq_iff_eq
modified theorem RelIso.apply_symm_apply
added theorem RelIso.eq_symm_apply
added theorem RelIso.refl_symm
added theorem RelIso.refl_trans
added theorem RelIso.self_comp_symm
modified theorem RelIso.self_trans_symm
modified theorem RelIso.symm_apply_apply
added theorem RelIso.symm_apply_eq
added theorem RelIso.symm_bijective
added theorem RelIso.symm_comp_self
added theorem RelIso.symm_symm
added theorem RelIso.symm_symm_apply
modified theorem RelIso.symm_trans_self
added theorem RelIso.trans_assoc
added theorem RelIso.trans_refl