fundamental property of division by units
authorhaftmann
Sun Oct 08 22:28:19 2017 +0200 (19 months ago)
changeset 6679839bb2462e681
parent 66797 9c9baae29217
child 66799 7ba45c30250c
fundamental property of division by units
src/HOL/Euclidean_Division.thy
     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -192,6 +192,10 @@
     1.4      by (auto intro!: euclidean_size_times_nonunit)
     1.5  qed
     1.6  
     1.7 +lemma unit_imp_mod_eq_0:
     1.8 +  "a mod b = 0" if "is_unit b"
     1.9 +  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
    1.10 +
    1.11  end
    1.12  
    1.13  class euclidean_ring = idom_modulo + euclidean_semiring