2493 lemma (in semidom_divide) prod_mset_minus: |
2493 lemma (in semidom_divide) prod_mset_minus: |
2494 assumes "a \<in># A" and "a \<noteq> 0" |
2494 assumes "a \<in># A" and "a \<noteq> 0" |
2495 shows "prod_mset (A - {#a#}) = prod_mset A div a" |
2495 shows "prod_mset (A - {#a#}) = prod_mset A div a" |
2496 using assms prod_mset_diff [of "{#a#}" A] by auto |
2496 using assms prod_mset_diff [of "{#a#}" A] by auto |
2497 |
2497 |
|
2498 lemma (in normalization_semidom) normalize_prod_mset_normalize: |
|
2499 "normalize (prod_mset (image_mset normalize A)) = normalize (prod_mset A)" |
|
2500 proof (induction A) |
|
2501 case (add x A) |
|
2502 have "normalize (prod_mset (image_mset normalize (add_mset x A))) = |
|
2503 normalize (x * normalize (prod_mset (image_mset normalize A)))" |
|
2504 by simp |
|
2505 also note add.IH |
|
2506 finally show ?case by simp |
|
2507 qed auto |
|
2508 |
2498 lemma (in algebraic_semidom) is_unit_prod_mset_iff: |
2509 lemma (in algebraic_semidom) is_unit_prod_mset_iff: |
2499 "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x \<in># A. is_unit x)" |
2510 "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x \<in># A. is_unit x)" |
2500 by (induct A) (auto simp: is_unit_mult_iff) |
2511 by (induct A) (auto simp: is_unit_mult_iff) |
2501 |
2512 |
2502 lemma (in normalization_semidom) normalize_prod_mset: |
2513 lemma (in normalization_semidom_multiplicative) normalize_prod_mset: |
2503 "normalize (prod_mset A) = prod_mset (image_mset normalize A)" |
2514 "normalize (prod_mset A) = prod_mset (image_mset normalize A)" |
2504 by (induct A) (simp_all add: normalize_mult) |
2515 by (induct A) (simp_all add: normalize_mult) |
2505 |
2516 |
2506 lemma (in normalization_semidom) normalized_prod_msetI: |
2517 lemma (in normalization_semidom_multiplicative) normalized_prod_msetI: |
2507 assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a" |
2518 assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a" |
2508 shows "normalize (prod_mset A) = prod_mset A" |
2519 shows "normalize (prod_mset A) = prod_mset A" |
2509 proof - |
2520 proof - |
2510 from assms have "image_mset normalize A = A" |
2521 from assms have "image_mset normalize A = A" |
2511 by (induct A) simp_all |
2522 by (induct A) simp_all |