mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(data/equiv/transfer_instance): avoid `let`, provide `nsmul`

Open urkud opened this issue 3 years ago • 1 comments

Also use @[simps] to generate some lemmas.

Open in Gitpod

urkud avatar Nov 04 '21 07:11 urkud

Should we wait for #10152 here? IMO that's the "main" API, this file is basically unused by all of algebra

eric-wieser avatar Nov 05 '21 08:11 eric-wieser