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.4    Copyright: Clemens Ballarin
     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"