Fixing Docstring in mathlib3

Stream: new members

[Kunhao Zheng]

Hi! I spot some typos in the docstring.

For example, this one #add_eq_add_iff_eq_and_eq has the same docstring as the above one #mul_eq_mul_iff_eq_and_eq

And this one #contravariant.to_left_cancel_semigroup. The docstring is talking about right cancel right?

Happy to help fix these docstrings. The first one is not trivial to me as the source uses @[to_additive] to autogenerate that theorem?

As this could be the first time I raise a PR on mathlib, following https://leanprover-community.github.io/contribute/index.html I post here for advice on how to do that. Thank you guys in advance!

[Kevin Buzzard]

If you want to contribute (and contributing docstrings is always welcome) you'll need an account on GitHub and you'll need to post your account userid so you can get access. Note that most theorems do not have docstrings, it's definitions and tactics which the community are strict on.

[Kunhao Zheng]

Kevin Buzzard said:

If you want to contribute (and contributing docstrings is always welcome) you'll need an account on GitHub and you'll need to post your account userid so you can get access. Note that most theorems do not have docstrings, it's definitions and tactics which the community are strict on.

sounds good. Thank you Kevin! My github userid is dyekuu

[Kyle Miller]

@Kunhao Zheng I've sent you an invite!

[Kunhao Zheng]

Kyle Miller said:

Kunhao Zheng I've sent you an invite!

Invite received! Thank you Kyle!