Theorem Equiv.toFun_as_coe

Modification history

2023-07-03 14:48
Mathlib/Logic/Equiv/Defs.lean
refactor: move all `register_simp_attr`s to 1 file (#5681) …
Modified Equiv.toFun_as_coeView on Github →
2022-12-23 13:50
Mathlib/Logic/Equiv/Defs.lean
chore: fix casing per naming scheme (#1183) …
Added Equiv.toFun_as_coeView on Github →