chore: golf a bit #212
Merged
chore: golf a bit #212
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
YaelDillies
reviewed
Nov 8, 2024
This reverts commit c8a4088.
YaelDillies
reviewed
Nov 10, 2024
FLT/Basic/Reductions.lean
Outdated
Comment on lines
259
to
265
| calc | ||
| 0 < a * a + a * b + b * b := ?_ | ||
| _ = _ := by ring | ||
| apply add_pos_of_nonneg_of_pos | ||
| apply add_nonneg (mul_self_nonneg _) h | ||
| apply mul_self_pos.mpr hb | ||
| exact add_pos_of_nonneg_of_pos (add_nonneg (mul_self_nonneg _) h) (mul_self_pos.mpr hb) | ||
| | inr h => | ||
| rw [sub_pos] | ||
| exact h.trans_le (sq_nonneg _) |
There was a problem hiding this comment.
Suggested change
| calc | |
| 0 < a * a + a * b + b * b := ?_ | |
| _ = _ := by ring | |
| apply add_pos_of_nonneg_of_pos | |
| apply add_nonneg (mul_self_nonneg _) h | |
| apply mul_self_pos.mpr hb | |
| exact add_pos_of_nonneg_of_pos (add_nonneg (mul_self_nonneg _) h) (mul_self_pos.mpr hb) | |
| | inr h => | |
| rw [sub_pos] | |
| exact h.trans_le (sq_nonneg _) | |
| rify | |
| calc | |
| (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity | |
| _ = (a + b) ^ 2 - a * b := by ring |
There was a problem hiding this comment.
Done, thanks.
There was a problem hiding this comment.
Looks like you only golfed the first branch of the proof, while my suggestion was to unify the branches. See #212 (comment)
Co-Authored-By: Yaël Dillies <[email protected]>
YaelDillies
reviewed
Nov 10, 2024
Co-Authored-By: Yaël Dillies <[email protected]>
Co-Authored-By: Yaël Dillies <[email protected]>
kbuzzard
approved these changes
Nov 11, 2024
FLT/Basic/Reductions.lean
Outdated
| apply Wiles_Frey P | ||
| exact Mazur_Frey P | ||
| theorem FreyPackage.false (P : FreyPackage) : False := | ||
| Wiles_Frey P (Mazur_Frey P) |
There was a problem hiding this comment.
I know this one can be golfed but I think it's nice to leave it as it is. We should really add documentation rather than golfing!
kbuzzard
reviewed
Nov 12, 2024
Co-authored-by: Kevin Buzzard <[email protected]>
…eLondon/FLT into pitmonticone/golf
|
Done @kbuzzard |
|
Thanks! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.