Commit 2022-04-19 10:05 5a4bae11
View on Github →feat(algebra/*/basic): add trivial lemmas (#13416)
These save you from having to fiddle with mul_one when you want to rewrite them the other way, or allow easier commutativity rewrites.
feat(algebra/*/basic): add trivial lemmas (#13416)
These save you from having to fiddle with mul_one when you want to rewrite them the other way, or allow easier commutativity rewrites.