equal
deleted
inserted
replaced
181 @{thm[display] relprime_dvd_mult} |
181 @{thm[display] relprime_dvd_mult} |
182 \rulename{relprime_dvd_mult} |
182 \rulename{relprime_dvd_mult} |
183 |
183 |
184 Another example of "insert" |
184 Another example of "insert" |
185 |
185 |
186 @{thm[display] mod_div_equality} |
186 @{thm[display] div_mult_mod_eq} |
187 \rulename{mod_div_equality} |
187 \rulename{div_mult_mod_eq} |
188 *} |
188 *} |
189 |
189 |
190 (*MOVED to Force.thy, which now depends only on Divides.thy |
190 (*MOVED to Force.thy, which now depends only on Divides.thy |
191 lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
191 lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
192 *) |
192 *) |