Mizarkommentare zu Gerd Fischers Lineare Algebra/ Grundbegriffe

1.1 Mengen und Abbildungen

1.1.1.

Mizar verfügt über keine $\ldots$-Notation für Mengen. $\{x\}$ ist {x} (TARSKI:def 1), $\{x,y\}$ ist {x,y} (TARSKI:def 3) und für explizit angegebene Mengen mit 3 bis 10 Elementen siehe ENUMSET1:def 1-8. $x\in X$ ist x in X aus HIDDEN (und damit immer ohne Referenz verfügbar). paarweise verschieden ist are_mutually_distinct und nur für 3 bis 7 Elemente in ZFMISC:def 5-9 definiert. Die (möglicherweise unendliche) Anzahl der Elemente einer Menge $X$ ist card X (CARD_1:def 2), die Anzahl der Elemente der explizit angegebenen Mengen (mit 0 bis 7 paarweise verschieden Elementen) ist CARD_1:27 ($n=0$), CARD_1:30 ($n=1$), CARD_2:57,58,59 ($n=2,3,4$), CARD_2:63 ($n=5$) und BORSUK_5:3,4 ($n=6,7$). Die Eigenschaft einer Menge, endlich zu sein, ist finite (FINSET_1:def 1).

Die leere Menge ist {} (XBOOLE_0:def 2) und die Eigenschaft einer Menge, leer zu sein, ist empty. Mit den üblichen requirements wird der Term X = {} genau so behandelt wie X is empty.

$X\subset Y$ ist X c= Y (TARSKI:def 3) und $X=Y$ ist in XBOOLE_0:def 10 definiert.

$\mathbb {N}$ wird in ORDINAL1:def 11 als omega eingeführt, das Synonym NAT wird in NUMBERS vergeben. Prinzip der vollständigen Induktion für Aussagen allgemein ist NAT_1:sch 2, aber keine Referenz für die nachfolgende, konkrete Aussage mit $M=\mathbb {N}$. Die Null, die in Mizar mit der leeren Menge identifiziert wird (ORDINAL1:def 13), ist nach Definition in NAT enthalten; $\mathbb {N} \setminus \{0\}$ ist NATPLUS (NAT_LAT:def 6).

$\mathbb {Z}$ ist INT (INT_1:def 1 oder NUMBERS:def 4) und $\mathbb {Q}$ ist RAT (RAT_1:def 1 oder NUMBERS:def 3). $\mathbb {R}$ ist REAL (NUMBERS:def 1): In Mizar werden die nichtnegativen reellen Zahlen über Dedekind-Schnitte eingeführt, siehe dafür ARYTM_2. $\mathbb {C}$ ist COMPLEX (NUMBERS:def 2), die Inklusionskette ist durch NUMBERS:17,14,12,11 gegeben.

1.1.2.

Für eine Eigenschaft $P$, die in Mizar zuvor mit defpred festgelegt wurde, entspricht $\{x\in X:x{\mbox{ hat Eigenschaft }}P\}$ dem Ausdruck { x where x is Element of X : P[x] }, welcher fest ins System eingebaut ist. Eine Variante hiervon ist die Notation the set of all x where x is special Element of X, wobei special stellvertretend für ein oder mehrere Attribute steht. Dies wird beispielsweise verwendet bei der Definition der Menge aller geraden Zahlen EvenNAT (FIB_NUM2:def 3).

Ähnlich zu 1.1.1. besitzt Mizar keine $\ldots$-Notation für Vereingung bzw. Schnitt einer endlichen Anzahl von Mengen. Aber $X\cup Y$ ist X \/ Y (XBOOLE_0:def 3) und $X\cap Y$ ist X /\ Y (XBOOLE_0:def 4).

Das Konzept einer durch eine Indexmenge $I$ induzierten Mengenfamilie $\{X_{i}\}_{i}\in I$ wird durch ManySortedSet beschrieben, welches einfach eine total I-defined Function (PBOOLE) ist (d.h. der Definitionsbereich der Abbildung ist ganz $I$). Dieses Konzept wird aber gar nicht benötigt, da allgemeine Vereingung bzw. Schnitt von Mengen in Mizar auf einer Menge von Mengen ohne Indexmenge definiert wird. Die entsprechenden Funktoren dazu sind union X (TARSKI:def 4) und meet X (SETFAM_1:def 1), wobei der Schnitt einer leeren Menge wieder als leer definiert wird. Ist dagegen jede Menge in $X$ Teilmenge einer Menge $D$, X is Subset-Family of D (SETFAM_1), so wird mit Intersection X (SETFAM_1:def 9) der Schnitt der leeren Menge als $D$ definiert (und sonst wie meet X). Keine Referenz für die Beispiele mit $X_{i}=[-i,i]$. Die Differenzmenge $X\setminus Y$ ist allgemeiner als X \ Y (XBOOLE_0:def 5) erklärt.

1.1.3.

Wie im Vorwort erwähnt werden in Fischers Buch Relationen nicht rigoros eingeführt. In Mizar ist eine Abbildung eine spezielle Relation (RELAT_1:def 1). Daher gelten viele offensichtliche Fakten über Abbildungen bereits allgemeiner für Relationen und sind daher in RELAT_1 statt in FUNCT_1 zu finden. Eine Abbildung $f$ ist eine Function (FUNCT_1:def 1). $f(x)$ ist f.x (FUNCT_1:def 2). Eine Abbildung von $X$ nach $Y$ ist dann eine Function of X, Y aus FUNCT_2, wobei die wesentlichen Eigenschaften in FUNCT_2:def 1, RELAT_1:def 18,19 eingebaut sind. $f=g$ ist FUNCT_1:2. $\operatorname {Abb} (X,Y)$ ist Funcs(X,Y) (FUNCT_2:def 2).

Multiplikation reeller Zahlen $ax$ ist als a*x definiert in XCMPLX_0:def 5 (und in XREAL_0 passend geclustert), $x^{2}$ ist x^2 (SQUARE_1:def 1; für allgemeine Potenzen reeller Zahlen siehe PREPOWER und POWER), ${\sqrt {x}}$ ist sqrt x (SQUARE_1:def 2). Dies sind nur die Vorschriften, die entsprechenden Abbildungen sind a multreal (RVSUM_1:5), sqrreal (RVSUM_1:def 2) und die Wurzeloperation kann dargestellt werden über sqrt id REAL+ (PARTFUN3:def 5, RELAT_1:def 10, ARYTM_2:def 2), keine direkte Referenz.

$f(M)$ ist f.:M (RELAT_1:def 13, FUNCT_1:def 6), $f^{-1}(N)$ ist f"N (RELAT_1:def 14, FUNCT_1:def 7). $f(M)\subset Y$ und $f^{-1}(N)\subset X$ sind in RELSET_1 verankert. $f^{-1}(y)$ ist f"{y} oder Coim(f,y) (RELAT_1:def 17). $f|M$ ist f | M (RELAT_1:def 11, geclustert in FUNCT_1).

1.1.4.

injektiv ist one-to-one (FUNCT_1:def 4), surjektiv ist onto (FUNCT_2:def 3), bijektiv ist bijective (FUNCT_2:def 4). Mizar reicht Injektivität, um eine Umkehrabbildung anzugeben: $f^{-1}$ ist f" (FUNCT_1:def 5, siehe auch RELAT_1:def 7), den passenden Definitions- und Wertebereich liefert FUNCT_2:25.

Der Satz hat keine direkte Referenz, kann aber aus FINSEQ_4:63,64 abgeleitet werden.

1.1.5.

$g\circ f$ ist g * f (RELAT_1:def 8, Reihenfolge des Funktors geändert und geclustert in FUNCT_1), die Anpassung des Definitions- und Wertebereichs erfolgt in RELSET_1.

Bemerkung über die Assoziativität ist RELAT_1:36.

Lemma ist gegeben durch FUNCT_1:39 und FUNCT_2:23, siehe auch FUNCT_1:31 und FUNCT_2:18.

1.1.6.

Wie zuvor ist auch eine $\ldots$-Notation für Tupel nicht direkt verfügbar. Ein Paar $(a,b)$ kann in Mizar mit der Kuratowski-Definition als [a,b] (TARSKI:def 5) dargestellt werden. Entsprechend gehört zu $A\times B$ [: A, B :] (ZFMISC_1:def 2). Tripel und Quadrupel gibt es als verschachtelte Kuratowski-Paare in XTUPLE_0:def 4,5, wo auch Funktoren definiert werden, um auf die Koordinaten zuzugreifen. Die entsprechenden Produkte aus 3 bzw. 4 Mengen sind dann in ZFMISC_1:def 3,4 definiert. MCART_1 und FUNCT_3 stellen verschiedene Arten der Projektionen bereit.

Eine andere Möglichkeit für die Tupeldarstellung von Elementen einer Menge $X$ ist als abbrechende Folge. Ein Tupel $x$ der Länge $n$ wäre dann einen-element FinSequence of X (CARD_1:def 7 und FINSEQ_1:def 4, siehe außerdem FINSEQ_1:def 2). Dies ist nichts anderes als eine Abbildung $x:\{1,\ldots ,n\}\rightarrow X$ (entsprechend ist $x_{i}$ dann x.i), wobei $\{1,\ldots ,n\}$ in Mizar durch Seg n (FINSEQ_1:def 1) gegeben ist. Die Menge aller Tupel über $X$ ist X* (FINSEQ_1:def 11), die Menge aller $n$-Tupel ist n-tuples_on X (FINSEQ_2:def 4). Funktoren für die direkte Angabe von Tupeln über ihre Koordinaten gibt es für $0\leq n\leq 8$: FINSEQ_1:def 6 ($n=0$), FINSEQ_1:def 8,9,10 ($n=1,2,3$), FINSEQ_4:def 7,8 ($n=4,5$) und AOFA_A00:def 4,5,6 ($n=6,7,8$).

Eine Variante der vorangegangenen Methode ist die Darstellung des Tupels als $x:\{0,\ldots ,n-1\}\rightarrow X$, wir beginnen die Zählung also nicht bei $1$ sondern bei $0$. Ein solches $x$ wäre dann eine n-element XFinSequence of X (AFINSQ_1; man beachte, dass das erste "X" Teil des Bezeichners ist und mit der Variable $X$ nichts zu tun hat). Der Definitionsbereich ist einfach $n=\{0,\ldots ,n-1\}$, da die natürlichen Zahlen so in Mizar definiert wurden (vgl. ORDINAL1). Es gibt nur explizite Funktoren für $0\leq n\leq 4$: AFINSQ_1:def 2 ($n=0$), AFINSQ_1:def 4,5,6 ($n=1,2,3$) und AFINSQ_1:def 14 ($n=4$).

Auf den ersten Blick mag die Tupel-Formalisierung startend mit $0$ aufgrund der vorangegangenen überflüssig erscheinen (gerade da sie erst später der MML hinzugefügt wurde), doch ist sie von Vorteil, wenn man z.B. nicht von vornherein weiß, ob eine vorliegende Folge abbricht oder nicht. AFINSQ_1 enthält auch Sätze, um zwischen den beiden Varianten nach Bedarf zu wechseln. In EXCHSORT werden diese beiden Herangehensweisen in einer Notation generalisiert.

Die vierte Variante formalisiert das allgemeine Produkt von Mengen. Sei $f:I\rightarrow X$ eine beliebige Funktion, die auf Mengen abbildet, dann bezeichnet product f (CARD_3:def 5) die Menge, die alle Funktionen $\varphi :I\rightarrow \bigcup _{i\in I}f(i)$ enthält mit $\varphi (i)\in f(i)$ für alle $i\in I$. Die Projektionen $\pi _{i}$ sind gegeben durch proj(f,i) (CARD_3:def 16). Falls $I\in \mathbb {N}$ und $f$ konstant, degeneriert die vierte zur dritten Variante.

Üblicherweise wird in Beweisen immer die einfachste Variante genommen, die ausreicht.

Eine (unendliche) Folge über $X$ ist eine sequence of X (NAT_1).

1.1.7.

Aufgrund der Definition einer Funktion als Relation gilt in Mizar $f=\Gamma _{f}$.

1.1.8.

Relation ist als ihr Graph definiert über RELAT_1:def 1, eine Relation als Teilmenge von $X\times Y$ wird in RELSET_1 geclustert. Bei einer Relation $R$ entspricht $a\sim b$ dann [a,b] in R. Viele Eigenschaften von Relationen finden sich in RELAT_2.

Eine Menge zusätzlich ausgestattet mit einer Relation ist eine RelStr (ORDERS_2). Sei S eine RelStr, dann wird die dazugehörige Menge mit the carrier of S (s. STRUCT_0) und die dazugehörige Relation mit the InternalRel of S gekennzeichnet. let a, b be Element of S, dann ist $a\sim b$ gegeben durch a <= b (ORDERS_2:def 5).

Eine Alternative zu dieser Notation, die ohne struct auskommt, gibt es in ARROW. Dort ist $a\sim b$ einer Relation $R$ gegeben durch a <=_R b (ARROW:def 4). Dies wird aber eher selten verwendet.

Beispiele a) Kann man nicht formalisieren.

b) Explizit als Funktor vorhanden: $x\leq y$ ist x <= y (XXREAL_0:def 5). Siehe auch die vielen Ungleichungen in XREAL_1.

c) Keine Referenz, aber die Äquivalenzklassen sind die Kreisringe und zu finden als Sphere(x,0) (TOPREAL9:def 3, s. auch EUCLID:def 5).

d) Die Kongruenzrelation ist Cong(m) (INT_4:def 1, s. auch INT_1:def 3,4).

Definition reflexiv ist reflexive (RELAT_2:def 1,9 bzw. ORDERS_2:def 2), symmetrisch ist symmetric (RELAT_2:def 3,11 bzw. NECKLACE:def 3) und transitiv ist transitive (RELAT_2:def 8,16 bzw. ORDERS_2:def 3). Eine Äquivalenzrelation auf $X$ ist eine Equivalence_Relation of X (EQREL_1). Äquivalenzklasse ist kein definierter mode in Mizar, aber die Äquivalenzklasse von $x$ unter $R$ ($A_{x}$ im Buch) ist Class(R,x) (in EQREL_1 als Synonym für Im(R,x) (RELAT_1:def 16) eingeführt), die Menge aller Äquivalenzklassen ($X/R$ im Buch) ist Class R (EQREL_1:def 3). Die angegebenen Eigenschaften sind geclustert in EQREL_1 (1) bzw. EQREL_1:22 (2) und EQREL_1:18,20 (3).

Bemerkung ist EQREL_1:24, siehe auch EQREL_1:def 4 in Verbindung mit EQREL_1:33 (letzteres ist auch ein Nachweis für Eigenschaft (1) $A\neq \emptyset$).

Eine Zerlegung $P$ von $X$ ist a_partition of X (EQREL_1:def 4). Die kanonische Abbildung für eine Zerlegung ist proj P (EQREL_1:def 9).

Aufgaben zu 1.1

1. (a) gegeben durch commutativity in XBOOLE_0:def 4,3 (b) XBOOLE_1:16,5 (c) XBOOLE_1:23,24 (d) XBOOLE_1:54,53
2. (a) RELAT_1:123 und RELAT_1:143 (b) FUNCT_1:76,75 (c) allgemeiner FUNCT_1:69 (d) FUNCT_1:68, RELAT_1:140,120,121; keine Referenz für Gegenbeispiel
3. (a) FUNCT_1:24, FUNCT_2:27 (b) FUNCT_1:25 und RELAT_1:28
4. (a) Addition ist definiert in XCMPLX_0:def 4 (und geclustert in XREAL_0), $f_{1}$ ist BINOP_2:def 9, keine Referenz für die Eigenschaften (b) keine Referenz (c) keine Referenz
5. gleichmächtig ist are_equipotent (WELLORD2:def 4, vgl. CARD_1:5), abzählbar unendlich ist denumerable (CARD_3:def 15). (a) TOPGEN_3:16,17 (b) TOPGEN_3:30 with TOPGEN_3:def 4 (c) CARD_2:31 with CARD_1:14
6. keine Referenz

1.2 Gruppen

1.2.1.

Eine Verknüpfung auf $G$ ist eine BinOp of G (BINOP_1). Einiges zu (b) findet sich in BINOP_2, sonst keine Referenz.

1.2.2.

Wie die meisten algebraischen Strukturen setzt sich eine Gruppe (Group/addGroup aus GROUP_1/GROUP_1A) in Mizar aus ihren Komponenten zusammen. Die zugrunde liegende Struktur ist multLoopStr /addMagma (ALGSTR_0), also einer Menge, die mit einer Verknüpfung und einer Eins versehen ist (im zweiten Fall wird sie später hinzugefügt). G1 ist associative/add-associative (GROUP_1:def 3/LVECT_1:def 3) und G2 ist Group-like/addGroup-like (GROUP_1:def 2/GROUP_1A:def 2). abelsch ist commutative/Abelian (GROUP_1:def 12/RLVECT_1:def 2). $a\ast b$ ist a * b/a + b (ALGSTR_0:def 18/1). Bei einer addGroup wird in Mizar nicht von Kommutativität ausgegangen, ebenso sind die Operatorsymbole fest an die entsprechende Struktur gebunden. Für eine Gruppe $G$ bezeichnet 1_G/0_G (GROUP_1:def 4/GROUP_1A:def 3) das neutrale Element. Für $a\in G$ bezeichnet a"/-a (GROUP_1:def 5/GROUP_1A:def 4) das neutrale Element. addGroup wird nur selten verwendet.

(a) ist SymGroup(X) (CAYLEY:def 2). (b) sind INT.Group (GR_CY_1:def 3), F_Rat (GAUSSINT:def 14) und wahlweise F_Real (VECTSP_1:def 5), G_Real (VECTSP_1:def 1 oder <REAL,+> aus MONOID_0:def 26; keine Referenz für $(\mathbb {R} _{+}^{\ast },\,\cdot \;)$. (c) keine Referenz.

1.2.3.

Bemerkung (a,b) Eindeutigkeit steckt in uniqueness von 1_G/0_G bzw. a"/-a; $a\cdot e=a$ bzw. $a\cdot a'$ wurde in Group-like/addGroup-like vorgegeben. (c) ist GROUP_1:def 5/GROUP_1A:def 4 (einschließlich involutiveness) und GROUP_1:17/GROUP_1A:16. (d) ist GROUP_1:6/GROUP_1A:6.

1.2.4.

$\tau _{a}$ ist a*/a+ (TOPGRP_1:def 1/GROUP_1A:def 44) und $_{a}\tau$ ist *a/+a (TOPGRP_1:def 2/GROUP_1A:def 45).

Lemma Bijektivität ist geclustert in TOPGRP_1/GROUP_1A. Keine Referenz für andere Richtung.

1.2.5.

Keine Referenz für das Tabellenverfahren, aber $G_{2/3/4}$ ist isomorph zu INT.Group(2/3/4) (GR_CY_1:def 5) bzw. Z/Z(2/3/4) (GROUP_14:def 1; das / in Z/Z ist Teil des Bezeichners), keine Referenz für $G_{4}^{\circ }$.

1.2.6.

Definition Untergruppe von G ist Subgroup of G (GROUP_2:50-52/GROUP_1A:96-98). Ein Homomorphismus zwischen $G$ und $H$ ist ein Homomorphism of G, H (GROUP_6, s. auch GROUP_6:def 6). Kein spezieller Bezeichner für bijektive Homomorphismen.

Bemerkung 1 steckt in existence von GROUP_2:def 5/GROUP_1A:def 15, die induzierte Verknüpfung ist einfach (the multF of G)||the carrier of H (REALSET1:def 2) (oder entsprechend the addF für addGroup).

Bemerkung 2 (a) GROUP_6:31 (b) GROUP_6:32 (c) GROUP_6:62

Beispiele (a) keine Referenz (b) teilweise indirekt mit SIN_COS:def 23 und SIN_COS:47,50,54 (c) keine Referenz, aber $m\mathbb {Z}$ ist m * INT (MEMBER_1:def 20).

1.2.7.

$r+m\mathbb {Z}$ ist r + m * INT (MEMBER_1:def 14). Eine andere Darstellung von 0/1 + 2 * NAT ist EvenNAT/OddNAT (NUMERAL2:def 1/2). $a\cong b\mod m$ ist a,b are_congruent_mod m (INT_1:def 4), mod can be found in INT_1:def 10. Keine Referenz für die Äquivalenzklassen als ebensolche, aber für $\mathbb {Z} /m\mathbb {Z}$ siehe GR_CY_1:def 5 bzw. GROUP_14:def 1, für allgemein Quotientengruppen $G/N$ siehe G ./. N (GROUP_6:def 4).

Aufgaben zu 1.2

1. keine Referenz
2. keine Referenz
3. keine Referenz
4. $\operatorname {erz} (A)$ ist gr A (GROUP_4:def 4), (i-ii) sind in der MML-Definition enthalten, und die Buchdefinition ist ersichtlich durch GROUP_4:28 in Verbindung mit GROUP_4:def 2 und GROUP_4:def 3.
5. $d$ entspricht Rotation(1,2,2,2*PI/n) (MATRTOP3:def 3) und $s$ entspricht AxialSymmetry(1,2) (MATRTOP3:def 2). Keine Referenz für $D_{n}$ oder die Aufgaben.
6. zyklisch ist cyclic (GR_CY_1:def 7) (a) keine Referenz (b) GR_CY_2:15,16
7. s. GROUP_2,3,6, keine Referenz für $\mathbb {Z} /m\mathbb {Z}$ in diesem Sinne.
8. keine Referenz

1.3 Ringe, Körper und Polynome

1.3.1.

Definition Ring ist in VECTSP_1 definiert (s. auch RLVECT_1:def 2,3,4, ALGSTR_0:def 11, GROUP_1:def 3, VECTSP_1:def 6,7). Für einen Ring $R$ ist die Null mit 0.R (STRUCT_0:def 6) und die Eins mit 1.R (STRUCT_0:def 7) ausgezeichnet, die Eigenschaft der Eins nach Buch steckt in well-unital (VECTSP_1:def 6). kommutativ ist commutative (GROUP_1:def 12).

Bemerkung ist VECTSP_1:6,7.

Beispiele (a) sind INT.Ring (INT_3:def 3), F_Rat (GAUSSINT:def 14) und F_Real (VECTSP_1:def 5) (b) ist RRing(I) (FUNCSDOM:def 7 und FUNCSDOM:26) (c) $\mathbb {Z} /m\mathbb {Z}$ als Ring ist INT.Ring(m) (INT_3:def 12), Synonym Z/m in RING_3 und falls $m$ prim, GF(m) in EC_PF_1.

1.3.2.

Definition nullteilerfrei ist domRing-like (VECTSP_2:def 1)

Bemerkung Eine Richung ist mit VECTSP_2:1 geclustert in INT_3, die andere Richtung in RING_5.

Definition Teilring ist Subring (C0SP1:def 3), Homomorphismus ist RingHomomorphism (QUOFIELD, s. RINGCAT1:def 1, VECTSP_1:def 20, GROUP_6:def 6, GROUP_1:def 13). Keine Referenz fürs Beispiel, aber vgl. RING_3

1.3.3.

Definition Ein Körper ist ein Field (VECTSP_1, s. auch STRUCT_0:def 8, VECTSP_1:def 9 und GROUP_1:def 12).

Bemerkung (a) STRUCT_0:def 8 (b) VECTSP_1:6,7 bzw. VECTSP_1:12 (c) VECTSP_1:12 (d) VECTSP_1:8-10 (e) VECTSP_1:5

1.3.4.

Beispiele für Körper (a) F_Rat (GAUSSINT:def 14) und F_Real (VECTSP_1:def 5) (b) F_Complex (COMPLFLD:def 1, s. unten) (c) GF(2) (mit INT_2:28) (d) geclustert in RING_3

Bemerkung keine Referenz

Definition ist RING_3:def 5

Lemma ist RING_3:86 mit VECTSP_2:1

Komplexe Zahlen

s. hier

1.3.5.

Wie das Buch schon andeutet, ist das Konzept der Unbekannten mathematisch nicht allzu leicht zu fassen. In der MML wird wie folgt vorgegangen:

In PRE_POLY wird für eine Menge $X$ ein bag of X als eine Funktion von $X$ nach $\mathbb {N}$ definiert, die nur an endlich vielen Stellen ungleich Null ist. Ein bag stellt ein Produkt von Potenzen mehrer Unbekannter dar, z.B. entspräche <% 2, 1, 4 %> (AFINSQ_1:def 6, für $X=\{0,1,2\}$) etwa dem Ausdruck $x^{2}yz^{4}$ (oder genauer $x_{0}^{2}x_{1}x_{2}^{4}$). Die Gesamtheit aller bag of X ist Bags X (PRE_POLY:def 12); Bag 1 entspräche etwa $\{1,x,x^{2},x^{3},\ldots \}$. Eine formale Potenzreihe über einer Struktur $S$ (z.B. Gruppe, Ring, Körper) ist dann eine Series of X, S (POLYNOM1), was einfach eine Funktion ist, die jedem bag (also Ausdruck wie z.B. $x^{2}yz^{4}$) einen Koeffizienten in $S$ zuordnet. Etwa ist das konstante Null- bzw. Eins-Polynom 0_(n, S) (POLYNOM1:def 8) bzw. 1_(n, S) (POLYNOM1:def 9), wobei $n$ hier die Anzahl der Variablen darstellt. Ein Polynomial of n, S (POLYNOM1) ist dann eine formale Potenzreihe, in der alle bis auf endlich viele der möglichen Koeffizienten gleich Null sind. POLYNOM3 bietet eine vereinfachte, alternative Notation an, wenn man nur Polynome in einer Variablen braucht: Dort ist ein Polynom einfach eine Funktion von einem Anfangsstück von $\mathbb {N}$ auf die Koeffizienten des Polynoms, z.B. entspräche <% 2, 1, 4 %> dem Polynom $4x^{2}+x+2$. Das Polynomial of S ist einfach ein Synonym in POLYNOM3 für AlgSequence of S (ALGSEQ_1).

$K[t]$ ist Polynom-Ring(1, K) (POLYNOM1:def 11) bzw. Polynom-Ring K (POLYNOM3:def 10). $\operatorname {deg} f$ ist degree f (HURWITZ_2, dort auch als Synonym deg f), wobei abweichend vom Buch $\operatorname {deg} 0$ als $-1$ definiert ist. $a_{n}$ ist Leading-Coefficient(f) (RATFUNC1:def 6, dort auch als Synonym LC(f)), normiert ist normalized (RATFUNC1:def 7). Für $a\in K$ ist $f(a)$ durch eval(f,a) (POLYNOM2:def 4 bzw. POLYNOM4:def 2) gegeben, die Evaluierungsfunktionen durch Polynom-Evaluation(n,K,a) (POLYNOM2:def 5) bzw. Polynom-Evaluation(K,a) (POLYNOM4:def 3).

Beispiel keine Referenz

1.3.6.

$f+g$ ist f + g (POLYNOM1:def 6 bzw. geclustert in POLYNOM3; s. auch VFUNCT_1:def 1 bzw. NORMSP_1:def 2). $f\cdot g$ ist f *' g (POLYNOM1:def 10 bzw. POLYNOM3:def 9). $f$ teilt $h$ ist f divides h (RING_4:def 3 oder HURWITZ:34).

Bemerkung $K[t]$ als kommutativer Ring ist geclustert in POLYNOM1 bzw. POLYNOM3. Die Gradeigenschaft ist HURWITZ:23, die Formalität ist über POLYNOM3:34 geklärt.

1.3.7.

Satz Existenz und Eindeutigkeit ist in der Definition von f div g (HURWITZ:def 5) gegeben.

Beispiel keine Referenz

1.3.8.

$x$ ist eine Nullstelle von $f$ ist x is_a_root_of f (POLYNOM5:def 7).

Beispiele (a) keine Referenz (b) keine Referenz

Lemma (1) HURWITZ:33 (s. auch HURWITZ:def 3) (2) HURWITZ:36

Korollar 1 RING_5:22

Korollar 2 keine Referenz

Definition $\mu (f;x)$ ist multiplicity(f, x) (UPROOTS:def 8). Die direkte Folgerung ist UPROOTS:52. Keine Referenz für die Beziehung mit den Ableitungen.

1.3.9.

Keine Referenz für den allgemeinen Fall ($g$ beliebig), aber das Zerfallen eines normierten Polynoms in Linearfaktoren über einem algebraisch geschlossenen Körper ist UPROOTS:65.

Fundamentalsatz der Algebra POLYNOM5:74

Korollar folgt aus UPROOTS:65 und RING_4:23.

1.3.10.

Lemma keine Referenz

Hilfssatz keine Referenz

Theorem keine Referenz

Korollar keine Referenz

Die Nullstelle eines Polynoms vom Grad 1 ist durch POLYVIE1:9 gegeben. Für die Lösungsformeln für Gleichungen 2. bis 4. Grades siehe POLYEQ_1-5. Keine Referenz für die Unlösbarkeit von Gleichungen fünften Grades oder höher.

1.3.11.

Keine Referenz für elementarsymmetrische Funktionen.

Vorzeichenregel keine Referenz

Vorzeichenregel von Descartes keine Referenz

Lemma keine Referenz

Aufgaben zu 1.3

1. keine Referenz
2. keine Referenz
3. keine Referenz
4. keine Referenz
5. keine Referenz
6. keine Referenz
7. keine Referenz
8. keine Referenz
9. keine Referenz
10. Die Äquivalenzrelation ist implizit über QUOFIELD:def 4 gegeben. Die Addition und Multiplikation sind gegeben durch QUOFIELD:def 6 und QUOFIELD:def 7 bzw. QUOFIELD:def 12 und QUOFIELD:def 13. Der Quotientenring ist gegeben über QUOFIELD:def 16; dass speziell $K(t)$ ein Körper ist, folgt aus den Eigenschaften von $K[t]$ und dem Clustering in QUOFIELD.
11. keine Referenz
12. Man kann natürlich einen solchen Beweis in Mizar verfassen, aber zu zeigen, dass dieser die Vorzeichenregel von Descartes sinnvoll nutzt und nicht etwa andere Sätze aus der MML ist nicht formalisierbar (außer durch Formalisierung der Beweise an sich, für die man die gesamte Theorie für die Beweise erneut aufbauen müsste).

1.4 Vektorräume

1.4.1.

Beispiele (a) $K^{n}$ ist n -VectSp_over K (PRVECT_1:def 5). ${\dot {+}}$ ist product(the addF of K,n) (PRVECT_1:def 1, s. auch FUNCOP_1:def 3 und FUNCT_3:def 7), $\cdot$ ist n -Mult_over F (PRVECT_1:def 4, s. auch FUNCOP_1:def 5 und FUNCT_3:def 7).

(b) Keine Referenz für $M(m\times n;K)$, aber $M(n\times n;K)$ ist n-Matrices_over K (MATRIX_1:def 1). $A{\dot {+}}B$ ist $A+B$ (MATRIX_1:def 5), $a\cdot A$ ist a * A (MATRIX_3:def 5).

(c) Keine Referenz als Funktion $\mathbb {R} \times \mathbb {C} \to \mathbb {C}$, aber s. BINOP_2:def 5.

(d) S. FVSUM_1:def 6 und Redefinition in POLYNOM1:def 1; bzw. POLYNOM5:def 4.

(e) $Abb(M,K)$ ist RealVectSpace(M) (FUNCSDOM:def 6) für $K=\mathbb {R}$ und ComplexVectSpace(M) (CFUNCDOM:def 6) für $K=\mathbb {C}$, sonst keine Referenz.

Definition Ein $K$-Vektorraum ist ein VectSp of K (VECTSP_1). Die Menge mit den zwei Verknüpfungen ist eine ModuleStr (VECTSP_1). V1 ist add-associative (RLVECT_1:def 3) right_zeroed (RLVECT_1:def 4) right_complementable (ALGSTR_0:def 16) Abelian (RLVECT_1:def 2) non empty (STRUCT_0:def 1). V2 ist vector-distributive scalar-distributive scalar-associative scalar-unital (VECTSP_1:def 13-16).

Bemerkung (a,b,d) VECTSP_1:14 (c) VECTSP_1:15

1.4.2.

Definition Ein Untervektorraum von $V$ ist ein Subspace of V (VECTSP_4:def 2, s. auch VECTSP_4:17,20,21 sowie VECTSP_4:34 in Kombination mit VECTSP_4:def 1).

Beispiele (a) $W_{1}$ ist (0).V (VECTSP_4:def 3), keine Referenz für die anderen Beispiele.

(b) MATRIX15:def 5

(c) ${\mathcal {C}}(\mathbb {R} ,\mathbb {R} )\subset \operatorname {Abb} (\mathbb {R} ,\mathbb {R} )$ als Vektorraum ist R_VectorSpace_of_C_0_Functions(REAL) (C0SP2:def 7). Keine Referenz für den Rest.

1.4.3.

Satz steckt in VECTSP_4:def 2

Lemma Nur definiert für nicht-induzierte Familien: $\bigcap _{U\in M}U\subset V$ ist meet M (VECTSP_8:def 5). Spezialfall für zwei Untervektorräume $W_{1}\cap W_{2}$ ist W1 /\ W2 (VECTSP_5:def 2).

Beispiel keine Referenz

Bemerkung VECTSP_5:35

1.4.4.

Ähnlich wie Polynome ist eine Linearkombination in Mizar definiert als eine Funktion Linear_Combination of V (VECTSP_6:def 1), die jedem Vektor ein Skalar zuordnet und nur endlich vielen ein Skalar ungleich Null. Für eine Linearkombination $f$ wird der dazugehörige Vektor mit Sum f (VECTSP_6:def 6) angegeben. Für eine Teilmenge $A$ von $V$ ist $\operatorname {span} _{K}A$ gegeben durch Lin A (VECTSP_7:def 2). $\operatorname {span} _{K}\emptyset =\{0\}$ ist VECTSP_7:9. Keine Referenz für suggestive Notation.

Bemerkung (a) steckt in VECTSP_7:def 2 (b) VECTSP_9:16

Beispiele (a,c,d) keine Referenz (b) $e_{i}$ ist Base_FinSeq(n,i) (MATRIXR2:def 4, allgemeiner MATRIX14:def 2), die gesamte Basis ist RN_Base n (EUCLID_7:def 13, dort auch als solche geclustert).

1.4.5.

Da jede Linearkombination in Mizar implizit alle nicht angegebenen Vektoren mit einem Skalar gleich Null versieht, ist die Linearkombination des Nullvektors mit Nullskalaren in Mizar eindeutig und wird mit ZeroLC(V) (VECTSP_6:def 3) bezeichnet.

Definition Eine linear unabhängige Teilmenge $M$ von $V$ ist linearly-independent (VECTSP_7:def 1); keine Referenz für die Tupel-Definition. Dass die leere Menge linear unabhängig ist, ist in VECTSP_7 geclustert.

Lemma keine Referenz

Beispiele (a) geclustert in EUCLID_7 (b,c) keine Referenz

Bemerkung (a) VECTSP_7:3 (b) VECTSP_7:2 (c) entfällt aufgrund der Mizar-Definition (d) z.T. RANKNULL:21

Aufgaben zu 1.4

1. keine Referenz
2. VECTSP12:def 7
3. keine Referenz
4. $t$-periodisch ist t-periodic (FUNCT_9:def 1); keine Referenz für die Aussagen
5. keine direkte Referenz, aber s. RSSPACE:def 7,13, RSSPACE3:def 3, LP_SPACE:def 2
6. keine Referenz
7. keine Referenz
8. keine Referenz
9. keine Referenz
10. keine Referenz

1.5 Basis und Dimension

1.5.1.

Definition Keine spezielle Referenz für das Erzeugendensystem. Eine (nicht geordnete) Basis von $V$ ist eine Basis of V (VECTSP_7, s. VECTSP_7:def 3). endlich erzeugt ist finite-dimensional (MATRLIN:def 1). Für eine Basis $B$ ist durch card B (CARD_1:def 2) ihre Länge gegeben. Eine (geordnete) Basis (als Tupel) ist eine OrdBasis of V (MATRLIN:def 2).

Beispiele (a) implizit über VECTSP_7:9 und das Clustering dort (b) geclustert in EUCLID_7 (c,d,e) keine Referenz

1.5.2.

Satz (i => iv) VECTSP_9:15 (i => ii) implizit in VECTSP_9:14 (sonst) keine Referenz

Zusatz Existenz einer Basis ist geclustert in VECTSP_7, deren Unendlichkeit ergibt sich dann aus der Definition von endlich erzeugt.

1.5.3.

Basisauswahlsatz VECTSP_7:20, VECTSP_9:20

Theorem geclustert in VECTSP_7

1.5.4.

Austauschlemma allgemeiner als VECTSP_9:18

Austauschsatz allgemeiner als VECTSP_9:19

1.5.5.

Korollar 1 implizit über VECTSP_9:20

Korollar 2 uniqueness von VECTSP_9:def 1

Definition $\operatorname {dim} _{K}V$ ist dim V (VECTSP_9:def 1), allerdings ohne den unendlichen Fall.

Korollar 3 VECTSP_9:24,25,28

Basisergänzungssatz VECTSP_7:19

Beispiele (a) RLAFFIN3:4 (b) sinngemäß VECTSP_9:30,31 (c,d,e) keine Referenz

1.5.6.

Mizar hat das Konzept von Anfang an allgemein aufgezogen.

1.5.7.

Beispiel $E_{n}$ ist 1.(K,n) (MATRIX_1:def 3).

1. Multiplikation der $i$-ten Zeile mit $a$ ist ScalarXLine(A,i,a) (MATRIX12:def 2)
2. Addition der $j$-ten Zeile zur $i$-ten Zeile ist RlineXScalar(A,i,j,1) (MATRIX12:def 3)
3. Addition des $a$-fachen der $j$-ten Zeile zur $i$-ten Zeile ist RlineXScalar(A,i,j,a) (MATRIX12:def 3)
4. Vertauschen der $i$-ten mit der $j$-ten Zeile ist InterchangeLine(A,i,j) (MATRIX12:def 1)

Definition Keine spezielle Referenz für $\operatorname {ZR} (A)$, stattdessen Lin lines A (s. MATRIX13:103 und MATRIX_0:def 7).

Lemma z.T. MATRIX15:69, sonst keine Referenz

Satz keine explizite Referenz, aber s. MATRIX15:sch 1,2

Beispiel keine Referenz

1.5.8.

$^{t}A$ ist A@ (MATRIX_0:def 6); Rechenregeln: (1) MATRIX_6:23 (2) nur reell: MATRIXR1:30 (3) MATRIX_0:57

Definition Mizar definiert den Rang einer Matrix nicht über die Dimension des Zeilen- bzw. Spaltenraums sondern direkt the_rank_of (MATRIX13:def 4) als die Länge der größten squadratischen Submatrix, die aus $A$ durch Löschen von Zeilen und Spalten entstehen kann und Determinante ungleich Null hat.

Lemma implizit über MATRIX13:90,92 bzw. MATRIX13:123

Aufgaben zu 1.5

1. keine Referenz
2. keine Referenz
3. keine Referenz
4. keine Referenz
5. keine Referenz
6. keine Referenz
7. keine Referenz
8. keine Referenz
9. keine Referenz
10. keine Referenz
11. keine Referenz
12. keine Referenz

1.6 Summen von Vektorräumen

1.6.1.

Definition Nur gegeben für die Summe zweier Vektorräume, W1 + W2 (VECTSP_5:def 1), sonst keine Referenz.

Bemerkung (a) steckt in VECTSP_5:def 1 (b) implizit durch VECTSP_7:15 und VECTSP_7:11 (c) implizit durch VECTSP_9:32

Dimensionsformel für Summen VECTSP_9:32

1.6.2.

Lemma keine Referenz

Definition $V=W_{1}\oplus W_{2}$ ist V is_the_direct_sum_of W1, W2 (VECTSP_5:def 4).

1.6.3.

Satz (i => ii) implizit durch VECTSP12:9 (i => iii) VECTSP_5:def 4, VECTSP_9:34 (sonst) keine Referenz

Korollar $W'$ ist Linear_Compl of V (VECTSP_5:def 5)

1.6.4.

Definition keine Referenz

Beispiel keine Referenz

Satz keine Referenz

Aufgaben zu 1.6

1. keine Referenz
2. keine Referenz
3. $A$ ist (schief)symmetrisch ist A is (anti)symmetric (MATRIX_6:def 5,6); keine Referenz für die Aufgaben