equal
deleted
inserted
replaced
14 fixes x :: "real^'n" |
14 fixes x :: "real^'n" |
15 shows "(\<And>k. m k \<noteq> 0) \<Longrightarrow> ((y = (\<chi> k. m k * x$k)) \<longleftrightarrow> (\<chi> k. y$k / m k) = x)" |
15 shows "(\<And>k. m k \<noteq> 0) \<Longrightarrow> ((y = (\<chi> k. m k * x$k)) \<longleftrightarrow> (\<chi> k. y$k / m k) = x)" |
16 by auto |
16 by auto |
17 |
17 |
18 lemma lambda_swap_Galois: |
18 lemma lambda_swap_Galois: |
19 "(x = (\<chi> i. y $ Fun.swap m n id i) \<longleftrightarrow> (\<chi> i. x $ Fun.swap m n id i) = y)" |
19 "(x = (\<chi> i. y $ Transposition.transpose m n i) \<longleftrightarrow> (\<chi> i. x $ Transposition.transpose m n i) = y)" |
20 by (auto; simp add: pointfree_idE vec_eq_iff) |
20 by (auto; simp add: pointfree_idE vec_eq_iff) |
21 |
21 |
22 lemma lambda_add_Galois: |
22 lemma lambda_add_Galois: |
23 fixes x :: "real^'n" |
23 fixes x :: "real^'n" |
24 shows "m \<noteq> n \<Longrightarrow> (x = (\<chi> i. if i = m then y$m + y$n else y$i) \<longleftrightarrow> (\<chi> i. if i = m then x$m - x$n else x$i) = y)" |
24 shows "m \<noteq> n \<Longrightarrow> (x = (\<chi> i. if i = m then y$m + y$n else y$i) \<longleftrightarrow> (\<chi> i. if i = m then x$m - x$n else x$i) = y)" |