Theorem FunLike.coe_one_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_iffView on Github →
2026-06-05 14:31
Mathlib/Data/FunLike/IsApply.lean
feat(Data/FunLike): `coe_zero_iff` lemmas (#40260)
Added FunLike.coe_one_iffView on Github →