chore: fix typo ("loosing")

avigad · Jan 6, 2025 · dd0e13e · dd0e13e
1 parent db963f2
commit dd0e13e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C09_Linear_Algebra/S04_Bases.lean b/MIL/C09_Linear_Algebra/S04_Bases.lean
@@ -207,7 +207,7 @@ example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
   norm_num
 -- QUOTE.
 /- TEXT:
-In order to define matrices as functions without loosing the benefits of ``Matrix``
+In order to define matrices as functions without losing the benefits of ``Matrix``
 for type class synthesis, we can use the equivalence ``Matrix.of`` between functions
 and matrices. This equivalence is secretly defined using ``Equiv.refl``.