equal
deleted
inserted
replaced
511 ultimately show "\<exists>x\<in>I. I = carrier R #> x" |
511 ultimately show "\<exists>x\<in>I. I = carrier R #> x" |
512 by fast |
512 by fast |
513 qed |
513 qed |
514 |
514 |
515 |
515 |
516 (* Next lemma contributed by Paulo Emílio de Vilhena. *) |
|
517 |
|
518 text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing, |
516 text \<open>This next lemma would be trivial if placed in a theory that imports QuotRing, |
519 but it makes more sense to have it here (easier to find and coherent with the |
517 but it makes more sense to have it here (easier to find and coherent with the |
520 previous developments).\<close> |
518 previous developments).\<close> |
521 |
519 |
522 lemma (in cring) cgenideal_prod: |
520 lemma (in cring) cgenideal_prod: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
523 assumes "a \<in> carrier R" "b \<in> carrier R" |
521 assumes "a \<in> carrier R" "b \<in> carrier R" |
524 shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)" |
522 shows "(PIdl a) <#> (PIdl b) = PIdl (a \<otimes> b)" |
525 proof - |
523 proof - |
526 have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)" |
524 have "(carrier R #> a) <#> (carrier R #> b) = carrier R #> (a \<otimes> b)" |
527 proof |
525 proof |