Skip to content

Commit

Permalink
typos
Browse files Browse the repository at this point in the history
  • Loading branch information
@yannickseurin @avigad
yannickseurin authored and avigad committed Jan 6, 2025
1 parent de7399f commit ac9825e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,9 +346,9 @@ See the file `GaussianInt.lean
<https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean>`_.
Here we will instead carry out an argument that stays in the integers.
This illustrates an choice one commonly faces when formalizing mathematics.
This illustrates a choice one commonly faces when formalizing mathematics.
Given an argument that requires concepts or machinery that is not already
in the library, one has two choices: either formalizes the concepts or machinery
in the library, one has two choices: either formalize the concepts or machinery
needed, or adapt the argument to make use of concepts and machinery you
already have.
The first choice is generally a good investment of time when the results
Expand Down

0 comments on commit ac9825e

Please sign in to comment.