Home | Metamath
Proof Explorer Theorem List (p. 414 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | clnr 41301 | Extend class notation with the class of left Noetherian rings. |
class LNoeR | ||
Definition | df-lnr 41302 | A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ LNoeR = {π β Ring β£ (ringLModβπ) β LNoeM} | ||
Theorem | islnr 41303 | Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (π΄ β Ring β§ (ringLModβπ΄) β LNoeM)) | ||
Theorem | lnrring 41304 | Left-Noetherian rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β π΄ β Ring) | ||
Theorem | lnrlnm 41305 | Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π΄ β LNoeR β (ringLModβπ΄) β LNoeM) | ||
Theorem | islnr2 41306* | Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) & β’ π = (RSpanβπ ) β β’ (π β LNoeR β (π β Ring β§ βπ β π βπ β (π« π΅ β© Fin)π = (πβπ))) | ||
Theorem | islnr3 41307 | Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) β β’ (π β LNoeR β (π β Ring β§ π β (NoeACSβπ΅))) | ||
Theorem | lnr2i 41308* | Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (LIdealβπ ) & β’ π = (RSpanβπ ) β β’ ((π β LNoeR β§ πΌ β π) β βπ β (π« πΌ β© Fin)πΌ = (πβπ)) | ||
Theorem | lpirlnr 41309 | Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π β LPIR β π β LNoeR) | ||
Theorem | lnrfrlm 41310 | Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015.) |
β’ π = (π freeLMod πΌ) β β’ ((π β LNoeR β§ πΌ β Fin) β π β LNoeM) | ||
Theorem | lnrfg 41311 | Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
β’ π = (Scalarβπ) β β’ ((π β LFinGen β§ π β LNoeR) β π β LNoeM) | ||
Theorem | lnrfgtr 41312 | A submodule of a finitely generated module over a Noetherian ring is finitely generated. Often taken as the definition of Noetherian ring. (Contributed by Stefan O'Rear, 7-Feb-2015.) |
β’ π = (Scalarβπ) & β’ π = (LSubSpβπ) & β’ π = (π βΎs π) β β’ ((π β LFinGen β§ π β LNoeR β§ π β π) β π β LFinGen) | ||
Syntax | cldgis 41313 | The leading ideal sequence used in the Hilbert Basis Theorem. |
class ldgIdlSeq | ||
Definition | df-ldgis 41314* | Define a function which carries polynomial ideals to the sequence of coefficient ideals of leading coefficients of degree- π₯ elements in the polynomial ideal. The proof that this map is strictly monotone is the core of the Hilbert Basis Theorem hbt 41322. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ ldgIdlSeq = (π β V β¦ (π β (LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) | ||
Theorem | hbtlem1 41315* | Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π· = ( deg1 βπ ) β β’ ((π β π β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) | ||
Theorem | hbtlem2 41316 | Leading coefficient ideals are ideals. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) β π) | ||
Theorem | hbtlem7 41317 | Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πβπΌ):β0βΆπ) | ||
Theorem | hbtlem4 41318 | The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β€ π) β β’ (π β ((πβπΌ)βπ) β ((πβπΌ)βπ)) | ||
Theorem | hbtlem3 41319 | The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β π β β0) β β’ (π β ((πβπΌ)βπ) β ((πβπ½)βπ)) | ||
Theorem | hbtlem5 41320* | The leading ideal function is strictly monotone. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β πΌ β π½) & β’ (π β βπ₯ β β0 ((πβπ½)βπ₯) β ((πβπΌ)βπ₯)) β β’ (π β πΌ = π½) | ||
Theorem | hbtlem6 41321* | There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π = (LIdealβπ) & β’ π = (ldgIdlSeqβπ ) & β’ π = (RSpanβπ) & β’ (π β π β LNoeR) & β’ (π β πΌ β π) & β’ (π β π β β0) β β’ (π β βπ β (π« πΌ β© Fin)((πβπΌ)βπ) β ((πβ(πβπ))βπ)) | ||
Theorem | hbt 41322 | The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (Poly1βπ ) β β’ (π β LNoeR β π β LNoeR) | ||
Syntax | cmnc 41323 | Extend class notation with the class of monic polynomials. |
class Monic | ||
Syntax | cplylt 41324 | Extend class notatin with the class of limited-degree polynomials. |
class Poly< | ||
Definition | df-mnc 41325* | Define the class of monic polynomials. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ Monic = (π β π« β β¦ {π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1}) | ||
Definition | df-plylt 41326* | Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.) |
β’ Poly< = (π β π« β, π₯ β β0 β¦ {π β (Polyβπ ) β£ (π = 0π β¨ (degβπ) < π₯)}) | ||
Theorem | dgrsub2 41327 | 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β(πΉ βf β πΊ)) < π) | ||
Theorem | elmnc 41328 | Property of a monic polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β (π β (Polyβπ) β§ ((coeffβπ)β(degβπ)) = 1)) | ||
Theorem | mncply 41329 | A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β (Polyβπ)) | ||
Theorem | mnccoe 41330 | A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β ((coeffβπ)β(degβπ)) = 1) | ||
Theorem | mncn0 41331 | A monic polynomial is not zero. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β ( Monic βπ) β π β 0π) | ||
Syntax | cdgraa 41332 | Extend class notation to include the degree function for algebraic numbers. |
class degAA | ||
Syntax | cmpaa 41333 | Extend class notation to include the minimal polynomial for an algebraic number. |
class minPolyAA | ||
Definition | df-dgraa 41334* | 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ββ) β {0π})((degβπ) = π β§ (πβπ₯) = 0)}, β, < )) | ||
Definition | df-mpaa 41335* | 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 = (π₯ β πΈ β¦ (β©π β (Polyββ)((degβπ) = (degAAβπ₯) β§ (πβπ₯) = 0 β§ ((coeffβπ)β(degAAβπ₯)) = 1))) | ||
Theorem | dgraaval 41336* | 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ββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < )) | ||
Theorem | dgraalem 41337* | 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ββ) β {0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) | ||
Theorem | dgraacl 41338 | Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degAAβπ΄) β β) | ||
Theorem | dgraaf 41339 | 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 41340 | Upper bound on degree of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) (Proof shortened by AV, 29-Sep-2020.) |
β’ (((π β (Polyββ) β§ π β 0π) β§ (π΄ β β β§ (πβπ΄) = 0)) β (degAAβπ΄) β€ (degβπ)) | ||
Theorem | dgraa0p 41341 | 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βπ΄)) β ((πβπ΄) = 0 β π = 0π)) | ||
Theorem | mpaaeu 41342* | An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β β!π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1)) | ||
Theorem | mpaaval 41343* | Value of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) = (β©π β (Polyββ)((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0 β§ ((coeffβπ)β(degAAβπ΄)) = 1))) | ||
Theorem | mpaalem 41344 | Properties of the minimal polynomial of an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄) β (Polyββ) β§ ((degβ(minPolyAAβπ΄)) = (degAAβπ΄) β§ ((minPolyAAβπ΄)βπ΄) = 0 β§ ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1))) | ||
Theorem | mpaacl 41345 | Minimal polynomial is a polynomial. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (minPolyAAβπ΄) β (Polyββ)) | ||
Theorem | mpaadgr 41346 | Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β (degβ(minPolyAAβπ΄)) = (degAAβπ΄)) | ||
Theorem | mpaaroot 41347 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄)βπ΄) = 0) | ||
Theorem | mpaamn 41348 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1) | ||
Syntax | citgo 41349 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 41350 | Extend class notation with the class of algebraic integers. |
class β€ | ||
Definition | df-itgo 41351* | 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 41354. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ IntgOver = (π β π« β β¦ {π₯ β β β£ βπ β (Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Definition | df-za 41352 | 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 41353* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β (IntgOverβπ) = {π₯ β β β£ βπ β (Polyβπ)((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Theorem | aaitgo 41354 | The standard algebraic numbers πΈ are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ πΈ = (IntgOverββ) | ||
Theorem | itgoss 41355 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ ((π β π β§ π β β) β (IntgOverβπ) β (IntgOverβπ)) | ||
Theorem | itgocn 41356 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (IntgOverβπ) β β | ||
Theorem | cnsrexpcl 41357 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (πβπ) β π) | ||
Theorem | fsumcnsrcl 41358* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | cnsrplycl 41359 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β (PolyβπΆ)) & β’ (π β π β π) & β’ (π β πΆ β π) β β’ (π β (πβπ) β π) | ||
Theorem | rgspnval 41360* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π = β© {π‘ β (SubRingβπ ) β£ π΄ β π‘}) | ||
Theorem | rgspncl 41361 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π β (SubRingβπ )) | ||
Theorem | rgspnssid 41362 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π΄ β π) | ||
Theorem | rgspnmin 41363 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π) β β’ (π β π β π) | ||
Theorem | rgspnid 41364 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΄ β (SubRingβπ )) & β’ (π β π = ((RingSpanβπ )βπ΄)) β β’ (π β π = π΄) | ||
Theorem | rngunsnply 41365* | 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 41366* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β πΉ = (π β π β¦ if(π = πΎ, 1, 0))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π ((πΉβπ) Β· π΅) = β¦πΎ / πβ¦π΅) | ||
Syntax | cmend 41367 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 41368* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ MEndo = (π β V β¦ β¦(π LMHom π) / πβ¦({β¨(Baseβndx), πβ©, β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf (+gβπ)π¦))β©, β¨(.rβndx), (π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx), (Scalarβπ)β©, β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦))β©})) | ||
Theorem | algstr 41369 | Lemma to shorten proofs of algbase 41370 through algvsca 41374. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ π΄ Struct β¨1, 6β© | ||
Theorem | algbase 41370 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π΅ β π β π΅ = (Baseβπ΄)) | ||
Theorem | algaddg 41371 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( + β π β + = (+gβπ΄)) | ||
Theorem | algmulr 41372 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Γ β π β Γ = (.rβπ΄)) | ||
Theorem | algsca 41373 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π β π β π = (Scalarβπ΄)) | ||
Theorem | algvsca 41374 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Β· β π β Β· = ( Β·π βπ΄)) | ||
Theorem | mendval 41375* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΅ = (π LMHom π) & β’ + = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf (+gβπ)π¦)) & β’ Γ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) & β’ π = (Scalarβπ) & β’ Β· = (π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦)) β β’ (π β π β (MEndoβπ) = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©})) | ||
Theorem | mendbas 41376 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π LMHom π) = (Baseβπ΄) | ||
Theorem | mendplusgfval 41377* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) β β’ (+gβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf + π¦)) | ||
Theorem | mendplusg 41378 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) & β’ β = (+gβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π βf + π)) | ||
Theorem | mendmulrfval 41379* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) β β’ (.rβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) | ||
Theorem | mendmulr 41380 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = (.rβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | mendsca 41381 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ π = (Scalarβπ΄) | ||
Theorem | mendvscafval 41382* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) β β’ ( Β·π βπ΄) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) | ||
Theorem | mendvsca 41383 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) & β’ β = ( Β·π βπ΄) β β’ ((π β πΎ β§ π β π΅) β (π β π) = ((πΈ Γ {π}) βf Β· π)) | ||
Theorem | mendring 41384 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π β LMod β π΄ β Ring) | ||
Theorem | mendlmod 41385 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β LMod) | ||
Theorem | mendassa 41386 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β AssAlg) | ||
Theorem | idomrootle 41387* | No element of an integral domain can have more than π π-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (.gβ(mulGrpβπ )) β β’ ((π β IDomn β§ π β π΅ β§ π β β) β (β―β{π¦ β π΅ β£ (π β π¦) = π}) β€ π) | ||
Theorem | idomodle 41388* | Limit on the number of π-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β) β (β―β{π₯ β π΅ β£ (πβπ₯) β₯ π}) β€ π) | ||
Theorem | fiuneneq 41389 | 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.) |
β’ ((π΄ β π΅ β§ π΄ β Fin) β ((π΄ βͺ π΅) β π΄ β π΄ = π΅)) | ||
Theorem | idomsubgmo 41390* | 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 41391 | Any primitive π-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (((π β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) | ||
Theorem | proot1hash 41392 | 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βπ )) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β β§ π β (β‘π β {π})) β (β―β(β‘π β {π})) = (Οβπ)) | ||
Theorem | proot1ex 41393 | The complex field has primitive π-th roots of unity for all π. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπΊ) β β’ (π β β β (-1βπ(2 / π)) β (β‘π β {π})) | ||
Syntax | ccytp 41394 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 41395* | 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 = (π β β β¦ ((mulGrpβ(Poly1ββfld)) Ξ£g (π β (β‘(odβ((mulGrpββfld) βΎs (β β {0}))) β {π}) β¦ ((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) | ||
Theorem | isdomn3 41396 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (mulGrpβπ ) β β’ (π β Domn β (π β Ring β§ (π΅ β { 0 }) β (SubMndβπ))) | ||
Theorem | mon1pid 41397 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ 1 = (1rβπ) & β’ π = (Monic1pβπ ) & β’ π· = ( deg1 βπ ) β β’ (π β NzRing β ( 1 β π β§ (π·β 1 ) = 0)) | ||
Theorem | mon1psubm 41398 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ π = (Monic1pβπ ) & β’ π = (mulGrpβπ) β β’ (π β NzRing β π β (SubMndβπ)) | ||
Theorem | deg1mhm 41399 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = ((mulGrpβπ) βΎs (π΅ β { 0 })) & β’ π = (βfld βΎs β0) β β’ (π β Domn β (π· βΎ (π΅ β { 0 })) β (π MndHom π)) | ||
Theorem | cytpfn 41400 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP Fn β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |