Home | Metamath
Proof Explorer Theorem List (p. 378 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmnc 37701 | Extend class notation with the class of monic polynomials. |
Syntax | cplylt 37702 | Extend class notatin with the class of limited-degree polynomials. |
Poly< | ||
Definition | df-mnc 37703* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
Poly coeffdeg | ||
Definition | df-plylt 37704* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
Poly< Poly deg | ||
Theorem | dgrsub2 37705 | Subtracting two polynomials with the same degree and top coefficient gives a polynomial of strictly lower degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
deg Poly Poly deg coeff coeff deg | ||
Theorem | elmnc 37706 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
Poly coeffdeg | ||
Theorem | mncply 37707 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
Poly | ||
Theorem | mnccoe 37708 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
coeffdeg | ||
Theorem | mncn0 37709 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
Syntax | cdgraa 37710 | Extend class notation to include the degree function for algebraic numbers. |
degAA | ||
Syntax | cmpaa 37711 | Extend class notation to include the minimal polynomial for an algebraic number. |
minPolyAA | ||
Definition | df-dgraa 37712* | Define the degree of an algebraic number as the smallest degree of any nonzero polynomial which has said number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
degAA inf Poly deg | ||
Definition | df-mpaa 37713* | Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
minPolyAA Polydeg degAA coeffdegAA | ||
Theorem | dgraaval 37714* | Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Revised by AV, 29-Sep-2020.) |
degAA inf Poly deg | ||
Theorem | dgraalem 37715* | Properties of the degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
degAA Poly deg degAA | ||
Theorem | dgraacl 37716 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
degAA | ||
Theorem | dgraaf 37717 | Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
degAA | ||
Theorem | dgraaub 37718 | Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
Poly degAA deg | ||
Theorem | dgraa0p 37719 | A rational polynomial of degree less than an algebraic number cannot be zero at that number unless it is the zero polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
Poly deg degAA | ||
Theorem | mpaaeu 37720* | An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
Polydeg degAA coeffdegAA | ||
Theorem | mpaaval 37721* | Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
minPolyAA Polydeg degAA coeffdegAA | ||
Theorem | mpaalem 37722 | Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
minPolyAA Poly degminPolyAA degAA minPolyAA coeffminPolyAAdegAA | ||
Theorem | mpaacl 37723 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
minPolyAA Poly | ||
Theorem | mpaadgr 37724 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
degminPolyAA degAA | ||
Theorem | mpaaroot 37725 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
minPolyAA | ||
Theorem | mpaamn 37726 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
coeffminPolyAAdegAA | ||
Syntax | citgo 37727 | Extend class notation with the integral-over predicate. |
IntgOver | ||
Syntax | cza 37728 | Extend class notation with the class of algebraic integers. |
ℤ | ||
Definition | df-itgo 37729* | A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 37732. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use (Contributed by Stefan O'Rear, 27-Nov-2014.) |
IntgOver Poly coeffdeg | ||
Definition | df-za 37730 | Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
ℤ IntgOver | ||
Theorem | itgoval 37731* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
IntgOver Poly coeffdeg | ||
Theorem | aaitgo 37732 | The standard algebraic numbers are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
IntgOver | ||
Theorem | itgoss 37733 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
IntgOver IntgOver | ||
Theorem | itgocn 37734 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
IntgOver | ||
Theorem | cnsrexpcl 37735 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
SubRingℂfld | ||
Theorem | fsumcnsrcl 37736* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
SubRingℂfld | ||
Theorem | cnsrplycl 37737 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
SubRingℂfld Poly | ||
Theorem | rgspnval 37738* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
RingSpan SubRing | ||
Theorem | rgspncl 37739 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
RingSpan SubRing | ||
Theorem | rgspnssid 37740 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
RingSpan | ||
Theorem | rgspnmin 37741 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
RingSpan SubRing | ||
Theorem | rgspnid 37742 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
SubRing RingSpan | ||
Theorem | rngunsnply 37743* | Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
SubRingℂfld RingSpanℂfld Poly | ||
Theorem | flcidc 37744* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
Syntax | cmend 37745 | Syntax for module endomorphism algebra. |
MEndo | ||
Definition | df-mend 37746* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo LMHom Scalar Scalar Scalar | ||
Theorem | algstr 37747 | Lemma to shorten proofs of algbase 37748 through algvsca 37752. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar Struct | ||
Theorem | algbase 37748 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar | ||
Theorem | algaddg 37749 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar | ||
Theorem | algmulr 37750 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar | ||
Theorem | algsca 37751 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar Scalar | ||
Theorem | algvsca 37752 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
Scalar | ||
Theorem | mendval 37753* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
LMHom Scalar MEndo Scalar | ||
Theorem | mendbas 37754 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo LMHom | ||
Theorem | mendplusgfval 37755* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo | ||
Theorem | mendplusg 37756 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
MEndo | ||
Theorem | mendmulrfval 37757* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo | ||
Theorem | mendmulr 37758 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
MEndo | ||
Theorem | mendsca 37759 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo Scalar Scalar | ||
Theorem | mendvscafval 37760* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
MEndo Scalar | ||
Theorem | mendvsca 37761 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
MEndo Scalar | ||
Theorem | mendring 37762 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
MEndo | ||
Theorem | mendlmod 37763 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
MEndo Scalar | ||
Theorem | mendassa 37764 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
MEndo Scalar AssAlg | ||
Syntax | csdrg 37765 | Syntax for subfields (sub-division-rings). |
SubDRing | ||
Definition | df-sdrg 37766* | A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
SubDRing SubRing ↾s | ||
Theorem | issdrg 37767 | Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.) |
SubDRing SubRing ↾s | ||
Theorem | issdrg2 37768* | Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.) |
SubDRing SubRing | ||
Theorem | acsfn1p 37769* | Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
ACS | ||
Theorem | subrgacs 37770 | Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
SubRing ACS | ||
Theorem | sdrgacs 37771 | Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.) |
SubDRing ACS | ||
Theorem | cntzsdrg 37772 | Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.) |
mulGrp Cntz SubDRing | ||
Theorem | idomrootle 37773* | No element of an integral domain can have more than -th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
.gmulGrp IDomn | ||
Theorem | idomodle 37774* | Limit on the number of -th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mulGrp ↾s Unit IDomn | ||
Theorem | fiuneneq 37775 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
Theorem | idomsubgmo 37776* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
mulGrp ↾s Unit IDomn SubGrp | ||
Theorem | proot1mul 37777 | Any primitive -th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
mulGrp ↾s Unit mrClsSubGrp IDomn | ||
Theorem | proot1hash 37778 | If an integral domain has a primitive -th root of unity, it has exactly of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mulGrp ↾s Unit IDomn | ||
Theorem | proot1ex 37779 | The complex field has primitive -th roots of unity for all . (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mulGrpℂfld ↾s | ||
Syntax | ccytp 37780 | Syntax for the sequence of cyclotomic polynomials. |
CytP | ||
Definition | df-cytp 37781* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
CytP mulGrpPoly1ℂfld g mulGrpℂfld ↾s var1ℂfldPoly1ℂfldalgScPoly1ℂfld | ||
Theorem | isdomn3 37782 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
mulGrp Domn SubMnd | ||
Theorem | mon1pid 37783 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
Poly1 Monic1p deg1 NzRing | ||
Theorem | mon1psubm 37784 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
Poly1 Monic1p mulGrp NzRing SubMnd | ||
Theorem | deg1mhm 37785 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
deg1 Poly1 mulGrp ↾s ℂfld ↾s Domn MndHom | ||
Theorem | cytpfn 37786 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
CytP | ||
Theorem | cytpval 37787* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
mulGrpℂfld ↾s Poly1ℂfld var1ℂfld mulGrp algSc CytP g | ||
Theorem | fgraphopab 37788* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
Theorem | fgraphxp 37789* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
Theorem | hausgraph 37790 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
Syntax | ctopsep 37791 | The class of separable toplogies. |
TopSep | ||
Syntax | ctoplnd 37792 | The class of Lindelöf toplogies. |
TopLnd | ||
Definition | df-topsep 37793* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
TopSep | ||
Definition | df-toplnd 37794* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
TopLnd | ||
Theorem | ioounsn 37795 | The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.) |
Theorem | iocunico 37796 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
Theorem | iocinico 37797 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
Theorem | iocmbl 37798 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
Theorem | cnioobibld 37799* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider . See cniccibl 23607 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
Theorem | itgpowd 37800* | The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |