equal
deleted
inserted
replaced
1616 lemma add_eq_0_iff: |
1616 lemma add_eq_0_iff: |
1617 fixes x y :: "'a::group_add" |
1617 fixes x y :: "'a::group_add" |
1618 shows "x + y = 0 \<longleftrightarrow> y = - x" |
1618 shows "x + y = 0 \<longleftrightarrow> y = - x" |
1619 by (auto dest: minus_unique) |
1619 by (auto dest: minus_unique) |
1620 |
1620 |
1621 text {* TODO: no longer real-specific; rename and move elsewhere *} |
|
1622 lemma realpow_two_disj: |
|
1623 fixes x :: "'a::idom" |
|
1624 shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
|
1625 using realpow_two_diff [of x y] |
|
1626 by (auto simp add: add_eq_0_iff) |
|
1627 |
|
1628 text {* FIXME: declare this [simp] for all types, or not at all *} |
1621 text {* FIXME: declare this [simp] for all types, or not at all *} |
1629 lemma real_two_squares_add_zero_iff [simp]: |
1622 lemma real_two_squares_add_zero_iff [simp]: |
1630 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1623 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
1631 by (rule sum_squares_eq_zero_iff) |
1624 by (rule sum_squares_eq_zero_iff) |
1632 |
1625 |