diff --git a/MIL/C10_Linear_Algebra/S04_Bases.lean b/MIL/C10_Linear_Algebra/S04_Bases.lean index d2127c8..1c46063 100644 --- a/MIL/C10_Linear_Algebra/S04_Bases.lean +++ b/MIL/C10_Linear_Algebra/S04_Bases.lean @@ -25,7 +25,7 @@ of linear algebra in :math:`K^n` for some field :math:`K`. Here the main objects are vectors and matrices. For concrete vectors, one can use the ``![…]`` notation, where components are separated by commas. For concrete matrices we can use the ``!![…]`` notation, lines are separated by semi-colons -and components of lines are separated by colons. +and components of lines are separated by commas. When entries have a computable type such as ``ℕ`` or ``ℚ``, we can use the ``eval`` command to play with basic operations.