Commit 2026-06-08 12:41 dde63614

View on Github →

chore(Data/{FunLike/SetLike}): unprime coe_injective' (#40215) Since Coe.coe and CoeFun.coe are reducible, the primed version is unnecessary.

Estimated changes

deleted theorem DFunLike.coe_injective
deleted theorem SetLike.coe_injective