equal
deleted
inserted
replaced
1610 lemma realpow_two_diff: |
1610 lemma realpow_two_diff: |
1611 fixes x :: "'a::comm_ring_1" |
1611 fixes x :: "'a::comm_ring_1" |
1612 shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
1612 shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
1613 by (simp add: algebra_simps) |
1613 by (simp add: algebra_simps) |
1614 |
1614 |
1615 text {* TODO: move elsewhere *} |
|
1616 lemma add_eq_0_iff: |
|
1617 fixes x y :: "'a::group_add" |
|
1618 shows "x + y = 0 \<longleftrightarrow> y = - x" |
|
1619 by (auto dest: minus_unique) |
|
1620 |
|
1621 text {* FIXME: declare this [simp] for all types, or not at all *} |
1615 text {* FIXME: declare this [simp] for all types, or not at all *} |
1622 lemma real_two_squares_add_zero_iff [simp]: |
1616 lemma real_two_squares_add_zero_iff [simp]: |
1623 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1617 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1624 by (rule sum_squares_eq_zero_iff) |
1618 by (rule sum_squares_eq_zero_iff) |
1625 |
1619 |