Theorem FunLike.coe_one_eq_id_iff

Modification history

2026-10-13 20:38

Mathlib/Algebra/Group/IsApply.lean

refactor(Algebra): make the arguments of `Is*Apply` implicit (#42704) …

Modified FunLike.coe_one_eq_id_iff View on Github →

2026-06-05 14:31

Mathlib/Data/FunLike/IsApply.lean

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

Added FunLike.coe_one_eq_id_iff View on Github →