From 7c58d207fe3d4090f1736989be6a6e0d5592567f Mon Sep 17 00:00:00 2001
From: fnHoj <110769980+fnHoj@users.noreply.github.com>
Date: Sat, 23 Aug 2025 14:53:27 +0800
Subject: [PATCH] Fix small typo
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Inline seperators of `!![…]` are commas instead of colons.
---
 MIL/C10_Linear_Algebra/S04_Bases.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.