Commit 2026-06-05 14:31 833b1ec7

View on Github →

feat(Data/FunLike): coe_zero_iff lemmas (#40260)

Estimated changes

Modified Mathlib/Data/FunLike/IsApply.lean

added theorem FunLike.coe_one_eq_id_iff

added theorem FunLike.coe_one_iff