Commit 2024-06-27 19:33 b0640e92

View on Github →

chore(AddConstMap): don't extend FunLike (#14201) Instead, take it as an argument as other bundled homs do. Also change the npow field in the Monoid instance so that coe_pow is a rfl lemma now.

Estimated changes