brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2025-10-10 06:51:13 +00:00
Code Issues Projects Releases Packages Activity

Web Archive Links

Browse source
This commit is contained in:
Brandon Rozek 2024-12-18 21:52:48 -05:00
parent c362493790
commit b560ee2cf2
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
8 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

2
content/blog/integer-sets-lean4.md
View file

@ -113,7 +113,7 @@ We can show this using a theorem from mathlib!
exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1
```
[(Quite the long name...)](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#eq_or_eq_neg_of_sq_eq_sq)
[(Quite the long name...)](https://web.archive.org/web/20240106030817/https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#eq_or_eq_neg_of_sq_eq_sq)
Lastly, we combine the two subset proofs to show equality