1586 lemma poly_mod_minus_left [simp]: |
1586 lemma poly_mod_minus_left [simp]: |
1587 fixes x y :: "'a::field poly" |
1587 fixes x y :: "'a::field poly" |
1588 shows "(- x) mod y = - (x mod y)" |
1588 shows "(- x) mod y = - (x mod y)" |
1589 using mod_smult_left [of "- 1::'a"] by simp |
1589 using mod_smult_left [of "- 1::'a"] by simp |
1590 |
1590 |
|
1591 lemma pdivmod_rel_add_left: |
|
1592 assumes "pdivmod_rel x y q r" |
|
1593 assumes "pdivmod_rel x' y q' r'" |
|
1594 shows "pdivmod_rel (x + x') y (q + q') (r + r')" |
|
1595 using assms unfolding pdivmod_rel_def |
|
1596 by (auto simp add: distrib degree_add_less) |
|
1597 |
|
1598 lemma poly_div_add_left: |
|
1599 fixes x y z :: "'a::field poly" |
|
1600 shows "(x + y) div z = x div z + y div z" |
|
1601 using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel] |
|
1602 by (rule div_poly_eq) |
|
1603 |
|
1604 lemma poly_mod_add_left: |
|
1605 fixes x y z :: "'a::field poly" |
|
1606 shows "(x + y) mod z = x mod z + y mod z" |
|
1607 using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel] |
|
1608 by (rule mod_poly_eq) |
|
1609 |
|
1610 lemma poly_div_diff_left: |
|
1611 fixes x y z :: "'a::field poly" |
|
1612 shows "(x - y) div z = x div z - y div z" |
|
1613 by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left) |
|
1614 |
|
1615 lemma poly_mod_diff_left: |
|
1616 fixes x y z :: "'a::field poly" |
|
1617 shows "(x - y) mod z = x mod z - y mod z" |
|
1618 by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left) |
|
1619 |
1591 lemma pdivmod_rel_smult_right: |
1620 lemma pdivmod_rel_smult_right: |
1592 "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk> |
1621 "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk> |
1593 \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r" |
1622 \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r" |
1594 unfolding pdivmod_rel_def by simp |
1623 unfolding pdivmod_rel_def by simp |
1595 |
1624 |