Commit ab3ade0d authored by immler's avatar immler
Browse files

fixed proofs

parent 85324e3788b7
......@@ -25,9 +25,9 @@ begin
(* TODO: Documentation and add references to computer algebra book *)
hide_const (open) Determinants.det
hide_const (open) Cartesian_Euclidean_Space.mat
hide_const (open) Cartesian_Euclidean_Space.row
hide_const (open) Cartesian_Euclidean_Space.vec
hide_const (open) Finite_Cartesian_Product.mat
hide_const (open) Finite_Cartesian_Product.row
hide_const (open) Finite_Cartesian_Product.vec
hide_const (open) Path_Connected.outside
hide_const (open) Linear_Algebra.orthogonal
hide_type (open) Finite_Cartesian_Product.vec
......@@ -1612,7 +1612,7 @@ lemma mem_set_find_indices [simp]: "i \<in> set (find_indices x xs) \<longleftri
lemma distinct_find_indices: "distinct (find_indices x xs)"
unfolding find_indices_def by simp
context module begin
context Module.module begin
definition lincomb_list
where "lincomb_list c vs = sumlist (map (\<lambda>i. c i \<odot>\<^bsub>M\<^esub> vs ! i) [0..<length vs])"
......@@ -1013,9 +1013,7 @@ lemma blinfuns_of_lvivl_eq: "blinfuns_of_lvivl x =
lemma range_blinfun_of_vmatrix[simp]: "range blinfun_of_vmatrix = UNIV"
apply auto
apply transfer
subgoal for x
unfolding linear_linear
by (auto intro!: matrix_works[symmetric])
subgoal for x by (rule image_eqI[where x="matrix x"]) auto
lemma blinfun_of_vmatrix_image:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment