11 theory Cartesian_Space |
11 theory Cartesian_Space |
12 imports |
12 imports |
13 Finite_Cartesian_Product Linear_Algebra |
13 Finite_Cartesian_Product Linear_Algebra |
14 begin |
14 begin |
15 |
15 |
|
16 subsection \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> |
|
17 |
16 definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}" |
18 definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}" |
17 |
19 |
18 lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def |
20 lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def |
19 using finite_Atleast_Atmost_nat by fastforce |
21 using finite_Atleast_Atmost_nat by fastforce |
20 |
22 |
21 lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" |
23 lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" |
22 unfolding cart_basis_def Setcompr_eq_image |
24 unfolding cart_basis_def Setcompr_eq_image |
23 by (rule card_image) (auto simp: inj_on_def axis_eq_axis) |
25 by (rule card_image) (auto simp: inj_on_def axis_eq_axis) |
24 |
26 |
25 interpretation vec: vector_space "(*s) " |
27 interpretation%important vec: vector_space "(*s) " |
26 by unfold_locales (vector algebra_simps)+ |
28 by unfold_locales (vector algebra_simps)+ |
27 |
29 |
28 lemma%unimportant independent_cart_basis: |
30 lemma%unimportant independent_cart_basis: |
29 "vec.independent (cart_basis)" |
31 "vec.independent (cart_basis)" |
30 proof (rule vec.independent_if_scalars_zero) |
32 proof (rule vec.independent_if_scalars_zero) |
448 qed |
450 qed |
449 also have "... = CARD('n)" by auto |
451 also have "... = CARD('n)" by auto |
450 finally show ?thesis . |
452 finally show ?thesis . |
451 qed |
453 qed |
452 |
454 |
453 interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a" |
455 interpretation%important vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a" |
454 by unfold_locales (simp_all add: algebra_simps) |
456 by unfold_locales (simp_all add: algebra_simps) |
455 |
457 |
456 lemmas [simp del] = vector_space_over_itself.scale_scale |
458 lemmas [simp del] = vector_space_over_itself.scale_scale |
457 |
459 |
458 interpretation vector_space_over_itself: finite_dimensional_vector_space |
460 interpretation vector_space_over_itself: finite_dimensional_vector_space |
459 "(*) :: 'a::field => 'a => 'a" "{1}" |
461 "(*) :: 'a::field => 'a => 'a" "{1}" |