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