mathlib3
6d2cf4ae
- fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip]
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip] * fix(doc/extra/tactic_writing): rename mul_left * one more fix
References
#902 - fix(doc/extra/tactic_writing): rename mul_left
Author
minchaowu
Committer
robertylewis
Parents
5f1329a2
Loading