equal
deleted
inserted
replaced
915 shows "linear f" |
915 shows "linear f" |
916 proof- |
916 proof- |
917 {fix v w |
917 {fix v w |
918 {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } |
918 {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } |
919 note th0 = this |
919 note th0 = this |
920 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
920 have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)" |
921 unfolding dot_norm_neg dist_norm[symmetric] |
921 unfolding dot_norm_neg dist_norm[symmetric] |
922 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
922 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
923 note fc = this |
923 note fc = this |
924 show ?thesis |
924 show ?thesis |
925 unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR |
925 unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR |