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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(geometry/euclidean): sum of angles of a triangle #2994

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(geometry/euclidean): sum of angles of a triangle #2994

wants to merge 4 commits into from

Conversation

jsm28
Copy link
Collaborator

@jsm28 jsm28 commented Jun 8, 2020

Item 27 from the 100-theorems list.

@jsm28
feat(geometry/euclidean): sum of angles of a triangle
eb501f7 
Item 27 from the 100-theorems list.
@jsm28 jsm28 added the awaiting-review The author would like community review of the PR label Jun 8, 2020
@jcommelin
Copy link
Member

Looks good to me, although some of the rw proofs are really long. I think I would take some of the show statements out of the rw block and put them before it as have H1 : ....
Alternatively, if you want to improve the readability some more, you could try to write the proof using calc blocks.

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 9, 2020
@jsm28
Copy link
Collaborator Author

jsm28 commented Jun 9, 2020

Moved those statements from show to have outside the rw as suggested. The expression being rearranged is long enough that I don't expect the proof to be very readable in any form, but the basic idea in those proofs is just field_simp, ring and everything else is just uninteresting rearrangement of the trigonometry, norms, inner products and square roots into a form field_simp can handle.

@jsm28 jsm28 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 9, 2020
jcommelin
jcommelin reviewed Jun 9, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

jcommelin
jcommelin approved these changes Jun 14, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 14, 2020
bors bot pushed a commit that referenced this pull request Jun 14, 2020
@jsm28
feat(geometry/euclidean): sum of angles of a triangle (#2994)
fdc326c 
Item 27 from the 100-theorems list.
@bors
Copy link

bors bot commented Jun 14, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(geometry/euclidean): sum of angles of a triangle [Merged by Bors] - feat(geometry/euclidean): sum of angles of a triangle Jun 14, 2020
@bors bors bot closed this Jun 14, 2020
@bors bors bot deleted the sum-angles-of-triangle branch June 14, 2020 08:36
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@jsm28 @cipher1024
feat(geometry/euclidean): sum of angles of a triangle (leanprover-com…
625a85f 
…munity#2994)

Item 27 from the 100-theorems list.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@jsm28 @jcommelin @semorrison