author | haftmann |
Sun, 16 Oct 2016 09:31:03 +0200 | |
changeset 64239 | de5cd9217d4c |
parent 64238 | b60a9752b6d0 |
child 64240 | eabf80376aab |
src/HOL/Rings.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Rings.thy Sun Oct 16 09:31:03 2016 +0200 +++ b/src/HOL/Rings.thy Sun Oct 16 09:31:03 2016 +0200 @@ -1918,6 +1918,10 @@ lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0" unfolding sgn_if by auto +lemma abs_sgn_eq_1 [simp]: + "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1" + by (simp add: abs_if) + lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)" by (simp add: sgn_if)