src/HOL/Rings.thy
changeset 64239 de5cd9217d4c
parent 64164 38c407446400
child 64240 eabf80376aab
equal deleted inserted replaced
64238:b60a9752b6d0 64239:de5cd9217d4c
  1916   unfolding sgn_if by auto
  1916   unfolding sgn_if by auto
  1917 
  1917 
  1918 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
  1918 lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0"
  1919   unfolding sgn_if by auto
  1919   unfolding sgn_if by auto
  1920 
  1920 
       
  1921 lemma abs_sgn_eq_1 [simp]:
       
  1922   "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1"
       
  1923   by (simp add: abs_if)
       
  1924 
  1921 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  1925 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
  1922   by (simp add: sgn_if)
  1926   by (simp add: sgn_if)
  1923 
  1927 
  1924 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1928 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
  1925   by (simp add: abs_if)
  1929   by (simp add: abs_if)