Theorem Function.mul_comm

Modification history

2025-12-01 17:54
MathlibTest/ToFun.lean
feat: `@[to_fun]` attribute for generating `fun _ => ...` form of lemmas (#31872) …
Added Function.mul_commView on Github →