From 6714a642e81958bafc135dcad89e17e0c5630d3a Mon Sep 17 00:00:00 2001
From: dnl232 <danconsa@hotmail.com>
Date: Wed, 1 May 2024 09:59:20 +0200
Subject: [PATCH] Module_ZF_1.thy - Submodules - Linear combinations

---
 IsarMathLib/Module_ZF.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/IsarMathLib/Module_ZF.thy b/IsarMathLib/Module_ZF.thy
index 1e3bb8f..22e61f4 100755
--- a/IsarMathLib/Module_ZF.thy
+++ b/IsarMathLib/Module_ZF.thy
@@ -279,7 +279,7 @@ qed
 
 text\<open>Multiplying by zero is zero.\<close>
 
-lemma(in module0) mult_zero:
+lemma (in module0) mult_zero:
   assumes "g\<in>\<M>"
   shows "\<zero> \<cdot>\<^sub>S g=\<Theta>"
 proof-
@@ -291,7 +291,7 @@ qed
 
 text \<open>Taking inverses in a module is just multiplying by $-1$\<close>
 
-lemma(in module0) inv_module:
+lemma (in module0) inv_module:
   assumes "g\<in>\<M>"
   shows "(\<rm>\<one>) \<cdot>\<^sub>S g = \<midarrow> g"
 proof-