Commit 2022-12-01 15:57 fc1a3ee9

View on Github →

feat: port Order.RelIso.Group (#813) mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c I would appreciate advice on naming lemmas about coercions, the porting guide doesn't say what to do.

Estimated changes

added theorem RelIso.apply_inv_self
added theorem RelIso.inv_apply_self
added theorem RelIso.mul_apply
added theorem RelIso.toFun_mul
added theorem RelIso.toFun_one