From 331bd046b7e2d2f964d9ae818fe8f398a109d58d Mon Sep 17 00:00:00 2001 From: dnl232 Date: Wed, 1 May 2024 13:05:51 +0200 Subject: [PATCH] Module_ZF_1.thy - Submodules - Linear combinations --- IsarMathLib/Module_ZF.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/IsarMathLib/Module_ZF.thy b/IsarMathLib/Module_ZF.thy index a8081f7..fe44a33 100755 --- a/IsarMathLib/Module_ZF.thy +++ b/IsarMathLib/Module_ZF.thy @@ -301,7 +301,7 @@ proof- also have "\=(\ \\) \\<^sub>S g" using module_ax2 A B assms unfolding ringsub_def by auto also have "\=\ \\<^sub>S g" using Ring_ZF_1_L3(7) A by auto also have "\=\" using mult_zero assms by auto - ultimately have "g+\<^sub>V ((\\) \\<^sub>S g)=\" by auto moreover + finally have "g+\<^sub>V ((\\) \\<^sub>S g)=\" by auto moreover from B have "H`(\\)\\\\" using H_val_type(2) by auto then have "(\\) \\<^sub>S g\\" unfolding End_def using apply_type assms by auto ultimately show ?thesis using mod_ab_gr.group0_2_L9(2) assms by auto