equal
deleted
inserted
replaced
1427 shows "ring_hom_cring P S Phi" |
1427 shows "ring_hom_cring P S Phi" |
1428 by unfold_locales (rule Phi) |
1428 by unfold_locales (rule Phi) |
1429 |
1429 |
1430 theorem UP_universal_property: |
1430 theorem UP_universal_property: |
1431 assumes S: "s \<in> carrier S" |
1431 assumes S: "s \<in> carrier S" |
1432 shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) & |
1432 shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) & |
1433 Phi (monom P \<one> 1) = s & |
1433 Phi (monom P \<one> 1) = s & |
1434 (ALL r : carrier R. Phi (monom P r 0) = h r)" |
1434 (ALL r : carrier R. Phi (monom P r 0) = h r)" |
1435 using S eval_monom1 |
1435 using S eval_monom1 |
1436 apply (auto intro: eval_ring_hom eval_const eval_extensional) |
1436 apply (auto intro: eval_ring_hom eval_const eval_extensional) |
1437 apply (rule extensionalityI) |
1437 apply (rule extensionalityI) |