Theorem RelIso.toFun_one

Modification history

2022-12-20 05:52

Mathlib/Order/RelIso/Group.lean

fix: reintroduce to_fun_as_coe as simp lemma (#931) …

Deleted RelIso.toFun_one View on Github →

2022-12-01 15:57

Mathlib/Order/RelIso/Group.lean

feat: port Order.RelIso.Group (#813) …

Added RelIso.toFun_one View on Github →