From 9daf81b58a8cf141ed632d25b847ccf80e91745c Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Mon, 16 Sep 2024 10:57:37 +0200 Subject: [PATCH] Fix build --- MIL/C09_Linear_Algebra/S04_Bases.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C09_Linear_Algebra/S04_Bases.lean b/MIL/C09_Linear_Algebra/S04_Bases.lean index b598887d..cc02cbc4 100644 --- a/MIL/C09_Linear_Algebra/S04_Bases.lean +++ b/MIL/C09_Linear_Algebra/S04_Bases.lean @@ -42,6 +42,7 @@ section matrices -- Multiplying matrices #eval !![1, 2; 3, 4] * !![3, 4; 5, 6] -- !![4, 6; 8, 10] +-- QUOTE. /- TEXT: It is important to understand that this use of ``#eval`` is interesting only for exploration, it is not meant to replace a computer algebra system such as Sage. @@ -86,7 +87,6 @@ Other familiar operations include the vector dot product, EXAMPLES: -/ -- QUOTE: --- QUOTE. /- TODO: make text for this section