equal
deleted
inserted
replaced
1599 lemma realpow_minus_mult: |
1599 lemma realpow_minus_mult: |
1600 fixes x :: "'a::monoid_mult" |
1600 fixes x :: "'a::monoid_mult" |
1601 shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n" |
1601 shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n" |
1602 by (simp add: power_commutes split add: nat_diff_split) |
1602 by (simp add: power_commutes split add: nat_diff_split) |
1603 |
1603 |
1604 text {* TODO: no longer real-specific; rename and move elsewhere *} |
|
1605 lemma realpow_two_diff: |
|
1606 fixes x :: "'a::comm_ring_1" |
|
1607 shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
|
1608 by (simp add: algebra_simps) |
|
1609 |
|
1610 text {* FIXME: declare this [simp] for all types, or not at all *} |
1604 text {* FIXME: declare this [simp] for all types, or not at all *} |
1611 lemma real_two_squares_add_zero_iff [simp]: |
1605 lemma real_two_squares_add_zero_iff [simp]: |
1612 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1606 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1613 by (rule sum_squares_eq_zero_iff) |
1607 by (rule sum_squares_eq_zero_iff) |
1614 |
1608 |