Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(analysis/exponential): real powers #647

Merged
merged 11 commits into from
Jan 30, 2019

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Jan 29, 2019

Also adopting the convention cpow for complex power and rpow for real power in naming lemmas.

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@johoelzl johoelzl merged commit aa944bf into leanprover-community:master Jan 30, 2019
@johoelzl johoelzl deleted the rpow branch January 30, 2019 09:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants