Skip to content

Commit

Permalink
fix: Migration typo
Browse files Browse the repository at this point in the history
  • Loading branch information
pimotte authored and PatrickMassot committed Dec 4, 2023
1 parent 30a4b11 commit eda3ee9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ be a square root of :math:`-1`. Thus we want
(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\
& = (ac - bd) + (bc + ad)i.
This explains the definition of ``hasMul`` below.
This explains the definition of ``Mul`` below.
BOTH: -/
namespace gaussInt

Expand Down

0 comments on commit eda3ee9

Please sign in to comment.