mathlib
458c833e
- chore(algebra/group/basic): Mark inv_involutive simp (#4744)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/group/basic): Mark inv_involutive simp (#4744) This means expressions like `has_inv.inv ∘ has_inv.inv` can be simplified
References
#4925 - Make prime-avoidance branch build
Author
eric-wieser
Parents
bb52355b
Loading