PR #902 fix(doc/extra/tactic_writing): rename mul_left

fix(doc/extra/tactic_writing): rename mul_left #902

robertylewis merged 2 commits into leanprover-community:master from minchaowu:master

fix(doc/extra/tactic_writing): rename mul_left

eb8ea223

minchaowu requested a review 7 years ago

one more fix

d013d71a

robertylewis merged 6d2cf4ae into master 7 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone