Commit 2022-11-10 22:45 e1cacd40

View on Github →

feat: port of Data.FunLike (#541) This is a very naive port of data.fun_like. I've never really engaged with this classes in mathlib3, and I haven't attempted to think about how they might work in Lean 4... This PR is really just provocation, hoping that @Vierkantor may come and have a look. :-)

Estimated changes

added structure CoolerHom
added theorem FunLike.coe_eq_coe_fn
added theorem FunLike.coe_fn_eq
added theorem FunLike.coe_injective
added theorem FunLike.exists_ne
added theorem FunLike.ext'
added theorem FunLike.ext'_iff
added theorem FunLike.ext
added theorem FunLike.ext_iff
added theorem FunLike.ne_iff
added theorem do_something
added theorem map_cool
added theorem map_op
added structure CoolerEmbedding
added theorem do_something
added theorem map_cool
added theorem map_op
added structure CoolerIso
added theorem do_something
added theorem map_cool