equal
deleted
inserted
replaced
64 and module_hom_linearI = module_hom_iff_linear[THEN iffD2] |
64 and module_hom_linearI = module_hom_iff_linear[THEN iffD2] |
65 |
65 |
66 context vector_space begin |
66 context vector_space begin |
67 |
67 |
68 sublocale module scale rewrites "module_hom = linear" |
68 sublocale module scale rewrites "module_hom = linear" |
69 by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+ |
69 by unfold_locales (fact vector_space_assms module_hom_eq_linear)+ |
70 |
70 |
71 lemmas\<comment> \<open>from \<open>module\<close>\<close> |
71 lemmas\<comment> \<open>from \<open>module\<close>\<close> |
72 linear_id = module_hom_id |
72 linear_id = module_hom_id |
73 and linear_ident = module_hom_ident |
73 and linear_ident = module_hom_ident |
74 and linear_scale_self = module_hom_scale_self |
74 and linear_scale_self = module_hom_scale_self |