src/HOL/Algebra/UnivPoly.thy
 changeset 20318 0e0ea63fe768 parent 20282 49c312eaaa11 child 20432 07ec57376051
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Aug 03 14:53:57 2006 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Aug 03 14:57:26 2006 +0200
1.3 @@ -5,9 +5,10 @@
1.5  *)
1.6
1.7 -header {* Univariate Polynomials *}
1.8 +theory UnivPoly imports Module begin
1.9
1.10 -theory UnivPoly imports Module begin
1.11 +
1.12 +section {* Univariate Polynomials *}
1.13
1.14  text {*
1.15    Polynomials are formalised as modules with additional operations for
1.16 @@ -161,7 +162,7 @@
1.17  qed
1.18
1.19
1.20 -subsection {* Effect of operations on coefficients *}
1.21 +subsection {* Effect of Operations on Coefficients *}
1.22
1.23  locale UP =
1.24    fixes R (structure) and P (structure)
1.25 @@ -219,7 +220,8 @@
1.26    from prem and R show "p x = q x" by (simp add: UP_def)
1.27  qed
1.28
1.29 -subsection {* Polynomials form a commutative ring. *}
1.30 +
1.31 +subsection {* Polynomials Form a Commutative Ring. *}
1.32
1.33  text {* Operations are closed over @{term P}. *}
1.34
1.35 @@ -401,7 +403,7 @@
1.36      (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
1.37
1.38
1.39 -subsection {* Polynomials form an Algebra *}
1.40 +subsection {* Polynomials Form an Algebra *}
1.41
1.42  lemma (in UP_cring) UP_smult_l_distr:
1.43    "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
1.44 @@ -445,7 +447,7 @@
1.45      (rule module.axioms algebra.axioms UP_algebra)+
1.46
1.47
1.48 -subsection {* Further lemmas involving monomials *}
1.49 +subsection {* Further Lemmas Involving Monomials *}
1.50
1.51  lemma (in UP_cring) monom_zero [simp]:
1.52    "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
1.53 @@ -603,7 +605,7 @@
1.54  qed
1.55
1.56
1.57 -subsection {* The degree function *}
1.58 +subsection {* The Degree Function *}
1.59
1.60  constdefs (structure R)
1.61    deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
1.62 @@ -887,7 +889,7 @@
1.63  qed
1.64
1.65
1.66 -subsection {* Polynomials over an integral domain form an integral domain *}
1.67 +subsection {* Polynomials over Integral Domains *}
1.68
1.69  lemma domainI:
1.70    assumes cring: "cring R"
1.71 @@ -948,7 +950,7 @@
1.72    by intro_locales (rule domain.axioms UP_domain)+
1.73
1.74
1.75 -subsection {* Evaluation Homomorphism and Universal Property*}
1.76 +subsection {* The Evaluation Homomorphism and Universal Property*}
1.77
1.78  (* alternative congruence rule (possibly more efficient)
1.79  lemma (in abelian_monoid) finsum_cong2:
1.80 @@ -1290,7 +1292,7 @@
1.81    done
1.82
1.83
1.84 -subsection {* Sample application of evaluation homomorphism *}
1.85 +subsection {* Sample Application of Evaluation Homomorphism *}
1.86
1.87  lemma UP_pre_univ_propI:
1.88    assumes "cring R"
```