Quelltext der Seite Mizarkommentare zu Gerd Fischers Lineare Algebra/ Grundbegriffe

<templatestyles src="Vorlage:OpenRewi/Inhaltsverzeichnis.css" />

__TOC__

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

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

<math>X\subset Y</math> ist <code>X c= Y</code> (<code>TARSKI:def 3</code>) und <math>X=Y</math> ist in <code>XBOOLE_0:def 10</code> definiert.

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

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

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

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

Das Konzept einer durch eine Indexmenge <math>I</math> induzierten Mengenfamilie <math>\{X_i\}_i\in I</math> wird durch <code>ManySortedSet</code> beschrieben, welches einfach eine <code>total I-defined Function</code> (<code>PBOOLE</code>) ist (d.h. der Definitionsbereich der Abbildung ist ganz <math>I</math>). 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 <code>union X</code> (<code>TARSKI:def 4</code>) und <code>meet X</code> (<code>SETFAM_1:def 1</code>), wobei der Schnitt einer leeren Menge wieder als leer definiert wird. Ist dagegen jede Menge in <math>X</math> Teilmenge einer Menge <math>D</math>, <code>X is Subset-Family of D</code> (<code>SETFAM_1</code>), so wird mit <code>Intersection X</code> (<code>SETFAM_1:def 9</code>) der Schnitt der leeren Menge als <math>D</math> definiert (und sonst wie <code>meet X</code>). Keine Referenz für die Beispiele mit <math>X_i=[-i,i]</math>. Die Differenzmenge <math>X \setminus Y</math> ist allgemeiner als <code>X \ Y</code> (<code>XBOOLE_0:def 5</code>) 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 <code>Relation</code> (<code>RELAT_1:def 1</code>). Daher gelten viele offensichtliche Fakten über Abbildungen bereits allgemeiner für Relationen und sind daher in <code>RELAT_1</code> statt in <code>FUNCT_1</code> zu finden. Eine Abbildung <math>f</math> ist eine <code>Function</code> (<code>FUNCT_1:def 1</code>). <math>f(x)</math> ist <code>f.x</code> (<code>FUNCT_1:def 2</code>). Eine Abbildung von <math>X</math> nach <math>Y</math> ist dann eine <code>Function of X, Y</code> aus <code>FUNCT_2</code>, wobei die wesentlichen Eigenschaften in <code>FUNCT_2:def 1</code>, <code>RELAT_1:def 18,19</code> eingebaut sind. <math>f=g</math> ist <code>FUNCT_1:2</code>. <math>\operatorname{Abb}(X,Y)</math> ist <code>Funcs(X,Y)</code> (<code>FUNCT_2:def 2</code>).

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

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

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

Der '''Satz''' hat keine direkte Referenz, kann aber aus <code>FINSEQ_4:63,64</code> abgeleitet werden.

===1.1.5.===
<math>g\circ f</math> ist <code>g * f</code> (<code>RELAT_1:def 8</code>, Reihenfolge des Funktors geändert und geclustert in <code>FUNCT_1</code>), die Anpassung des Definitions- und Wertebereichs erfolgt in <code>RELSET_1</code>.

'''Bemerkung''' über die Assoziativität ist <code>RELAT_1:36</code>.

'''Lemma''' ist gegeben durch <code>FUNCT_1:39</code> und <code>FUNCT_2:23</code>, siehe auch <code>FUNCT_1:31</code> und <code>FUNCT_2:18</code>.

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

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

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

Auf den ersten Blick mag die Tupel-Formalisierung startend mit <math>0</math> 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. <code>AFINSQ_1</code> enthält auch Sätze, um zwischen den beiden Varianten nach Bedarf zu wechseln. In <code>EXCHSORT</code> werden diese beiden Herangehensweisen in einer Notation generalisiert.

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

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

Eine (unendliche) Folge über <math>X</math> ist eine <code>sequence of X</code> (<code>NAT_1</code>).

===1.1.7.===
Aufgrund der Definition einer Funktion als Relation gilt in Mizar <math>f=\Gamma_f</math>.

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

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

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

'''Beispiele''' a) Kann man nicht formalisieren.

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

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

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

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

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

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

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

==1.2 Gruppen==

===1.2.1.===
Eine ''Verknüpfung'' auf <math>G</math> ist eine <code>BinOp of G</code> (<code>BINOP_1</code>). Einiges zu (b) findet sich in <code>BINOP_2</code>, sonst keine Referenz.

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

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

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

===1.2.4.===
<math>\tau_a</math> ist <code>a*</code>/<code>a+</code> (<code>TOPGRP_1:def 1</code>/<code>GROUP_1A:def 44</code>) und <math>_a\tau</math> ist <code>*a</code>/<code>+a</code> (<code>TOPGRP_1:def 2</code>/<code>GROUP_1A:def 45</code>).

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

===1.2.5.===
Keine Referenz für das Tabellenverfahren, aber <math>G_{2/3/4}</math> ist isomorph zu <code>INT.Group(2/3/4)</code> (<code>GR_CY_1:def 5</code>) bzw. <code>Z/Z(2/3/4)</code> (<code>GROUP_14:def 1</code>; das <tt>/</tt> in <code>Z/Z</code> ist Teil des Bezeichners), keine Referenz für <math>G^\circ_4</math>.

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

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

'''Bemerkung 2''' (a) <code>GROUP_6:31</code> (b) <code>GROUP_6:32</code> (c) <code>GROUP_6:62</code>

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

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

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

==1.3 Ringe, Körper und Polynome==
===1.3.1.===
'''Definition''' <code>Ring</code> ist in <code>VECTSP_1</code> definiert (s. auch <code>RLVECT_1:def 2,3,4</code>, <code>ALGSTR_0:def 11</code>, <code>GROUP_1:def 3</code>, <code>VECTSP_1:def 6,7</code>). Für einen Ring <math>R</math> ist die Null mit <code>0.R</code> (<code>STRUCT_0:def 6</code>) und die Eins mit <code>1.R</code> (<code>STRUCT_0:def 7</code>) ausgezeichnet, die Eigenschaft der Eins nach Buch steckt in <code>well-unital</code> (<code>VECTSP_1:def 6</code>). ''kommutativ'' ist <code>commutative</code> (<code>GROUP_1:def 12</code>).

'''Bemerkung''' ist <code>VECTSP_1:6,7</code>.

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

===1.3.2.===
'''Definition''' ''nullteilerfrei'' ist <code>domRing-like</code> (<code>VECTSP_2:def 1</code>)

'''Bemerkung''' Eine Richung ist mit <code>VECTSP_2:1</code> geclustert in <code>INT_3</code>, die andere Richtung in <code>RING_5</code>.

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

===1.3.3.===
'''Definition''' Ein ''Körper'' ist ein <code>Field</code> (<code>VECTSP_1</code>, s. auch <code>STRUCT_0:def 8</code>, <code>VECTSP_1:def 9</code> und <code>GROUP_1:def 12</code>).

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

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

'''Bemerkung''' keine Referenz

'''Definition''' ist <code>RING_3:def 5</code>

'''Lemma''' ist <code>RING_3:86</code> mit <code>VECTSP_2:1</code>

====Komplexe Zahlen====
s. [https://en.wikibooks.org/wiki/Mizar_Commentary_on_Walter_Rudin%27s_Principles_of_Mathematical_Analysis/The_Real_and_Complex_Number_Systems#The_Complex_Field 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 <code>PRE_POLY</code> wird für eine Menge <math>X</math> ein <code>bag of X</code> als eine Funktion von <math>X</math> nach <math>\mathbb{N}</math> definiert, die nur an endlich vielen Stellen ungleich Null ist. Ein <code>bag</code> stellt ein Produkt von Potenzen mehrer Unbekannter dar, z.B. entspräche <code><% 2, 1, 4 %></code> (<code>AFINSQ_1:def 6</code>, für <math>X=\{0,1,2\}</math>) etwa dem Ausdruck <math>x^2yz^4</math> (oder genauer <math>x_0^2x_1x_2^4</math>). Die Gesamtheit aller <code>bag of X</code> ist <code>Bags X</code> (<code>PRE_POLY:def 12</code>); <code>Bag 1</code> entspräche etwa <math>\{1,x,x^2,x^3,\ldots\}</math>. Eine formale Potenzreihe über einer Struktur <math>S</math> (z.B. Gruppe, Ring, Körper) ist dann eine <code>Series of X, S</code> (<code>POLYNOM1</code>), was einfach eine Funktion ist, die jedem <code>bag</code> (also Ausdruck wie z.B. <math>x^2yz^4</math>) einen Koeffizienten in <math>S</math> zuordnet. Etwa ist das konstante Null- bzw. Eins-Polynom <code>0_(n, S)</code> (<code>POLYNOM1:def 8</code>) bzw. <code>1_(n, S)</code> (<code>POLYNOM1:def 9</code>), wobei <math>n</math> hier die Anzahl der Variablen darstellt. Ein <code>Polynomial of n, S</code> (<code>POLYNOM1</code>) ist dann eine formale Potenzreihe, in der alle bis auf endlich viele der möglichen Koeffizienten gleich Null sind. <code>POLYNOM3</code> 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 <math>\mathbb{N}</math> auf die Koeffizienten des Polynoms, z.B. entspräche <code><% 2, 1, 4 %></code> dem Polynom <math>4x^2+x+2</math>. Das <code>Polynomial of S</code> ist einfach ein Synonym in <code>POLYNOM3</code> für <code>AlgSequence of S</code> (<code>ALGSEQ_1</code>).

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

'''Beispiel''' keine Referenz

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

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

===1.3.7.===

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

'''Beispiel''' keine Referenz

===1.3.8.===

''<math>x</math> ist eine Nullstelle von <math>f</math>'' ist <code>x is_a_root_of f</code> (<code>POLYNOM5:def 7</code>).

'''Beispiele''' (a) keine Referenz (b) keine Referenz

'''Lemma''' (1) <code>HURWITZ:33</code> (s. auch <code>HURWITZ:def 3</code>) (2) <code>HURWITZ:36</code>

'''Korollar 1''' <code>RING_5:22</code>

'''Korollar 2''' keine Referenz

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

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

'''Fundamentalsatz der Algebra''' <code>POLYNOM5:74</code>

'''Korollar''' folgt aus <code>UPROOTS:65</code> und <code>RING_4:23</code>.

===1.3.10.===
'''Lemma''' keine Referenz

'''Hilfssatz''' keine Referenz

'''Theorem''' keine Referenz

'''Korollar''' keine Referenz

Die Nullstelle eines Polynoms vom Grad 1 ist durch <code>POLYVIE1:9</code> gegeben. Für die Lösungsformeln für Gleichungen 2. bis 4. Grades siehe <code>POLYEQ_1-5</code>. 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===
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# Die Äquivalenzrelation ist implizit über <code>QUOFIELD:def 4</code> gegeben. Die Addition und Multiplikation sind gegeben durch <code>QUOFIELD:def 6</code> und <code>QUOFIELD:def 7</code> bzw. <code>QUOFIELD:def 12</code> und <code>QUOFIELD:def 13</code>. Der Quotientenring ist gegeben über <code>QUOFIELD:def 16</code>; dass speziell <math>K(t)</math> ein Körper ist, folgt aus den Eigenschaften von <math>K[t]</math> und dem Clustering in <code>QUOFIELD</code>.
# keine Referenz
# 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) <math>K^n</math> ist <code>n -VectSp_over K</code> (<code>PRVECT_1:def 5</code>). <math>\dot{+}</math> ist <code>product(the addF of K,n)</code> (<code>PRVECT_1:def 1</code>, s. auch <code>FUNCOP_1:def 3</code> und <code>FUNCT_3:def 7</code>), <math>\cdot</math> ist <code>n -Mult_over F</code> (<code>PRVECT_1:def 4</code>, s. auch <code>FUNCOP_1:def 5</code> und <code>FUNCT_3:def 7</code>).

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

(c) Keine Referenz als Funktion <math>\mathbb{R}\times\mathbb{C}\to\mathbb{C}</math>, aber s. <code>BINOP_2:def 5</code>.

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

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

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

'''Bemerkung''' (a,b,d) <code>VECTSP_1:14</code> (c) <code>VECTSP_1:15</code>

===1.4.2.===
'''Definition''' Ein ''Untervektorraum von <math>V</math>'' ist ein <code>Subspace of V</code> (<code>VECTSP_4:def 2</code>, s. auch <code>VECTSP_4:17,20,21</code> sowie <code>VECTSP_4:34</code> in Kombination mit <code>VECTSP_4:def 1</code>).

'''Beispiele''' (a) <math>W_1</math> ist <code>(0).V</code> (<code>VECTSP_4:def 3</code>), keine Referenz für die anderen Beispiele.

(b) <code>MATRIX15:def 5</code>

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

===1.4.3.===
'''Satz''' steckt in <code>VECTSP_4:def 2</code>

'''Lemma''' Nur definiert für nicht-induzierte Familien: <math>\bigcap_{U\in M} U\subset V</math> ist <code>meet M</code> (<code>VECTSP_8:def 5</code>). Spezialfall für zwei Untervektorräume <math>W_1\cap W_2</math> ist <code>W1 /\ W2</code> (<code>VECTSP_5:def 2</code>).

'''Beispiel''' keine Referenz

'''Bemerkung''' <code>VECTSP_5:35</code>

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

'''Bemerkung''' (a) steckt in <code>VECTSP_7:def 2</code> (b) <code>VECTSP_9:16</code>

'''Beispiele''' (a,c,d) keine Referenz (b) <math>e_i</math> ist <code>Base_FinSeq(n,i)</code> (<code>MATRIXR2:def 4</code>, allgemeiner <code>MATRIX14:def 2</code>), die gesamte Basis ist <code>RN_Base n</code> (<code>EUCLID_7:def 13</code>, 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 <code>ZeroLC(V)</code> (<code>VECTSP_6:def 3</code>) bezeichnet.

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

'''Lemma''' keine Referenz

'''Beispiele''' (a) geclustert in <code>EUCLID_7</code> (b,c) keine Referenz

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

===Aufgaben zu 1.4===
# keine Referenz
# <code>VECTSP12:def 7</code>
# keine Referenz
# ''<math>t</math>-periodisch'' ist <code>t-periodic</code> (<code>FUNCT_9:def 1</code>); keine Referenz für die Aussagen
# keine direkte Referenz, aber s. <code>RSSPACE:def 7,13</code>, <code>RSSPACE3:def 3</code>, <code>LP_SPACE:def 2</code>
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz

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

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

===1.5.2.===
'''Satz''' (i => iv) <code>VECTSP_9:15</code> (i => ii) implizit in <code>VECTSP_9:14</code> (sonst) keine Referenz

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

===1.5.3.===
'''Basisauswahlsatz''' <code>VECTSP_7:20</code>, <code>VECTSP_9:20</code>

'''Theorem''' geclustert in <code>VECTSP_7</code>

===1.5.4.===
'''Austauschlemma''' allgemeiner als <code>VECTSP_9:18</code>

'''Austauschsatz''' allgemeiner als <code>VECTSP_9:19</code>

===1.5.5.===
'''Korollar 1''' implizit über <code>VECTSP_9:20</code>

'''Korollar 2''' <code>uniqueness</code> von <code>VECTSP_9:def 1</code>

'''Definition''' <math>\operatorname{dim}_K V</math> ist <code>dim V</code> (<code>VECTSP_9:def 1</code>), allerdings ohne den unendlichen Fall.

'''Korollar 3''' <code>VECTSP_9:24,25,28</code>

'''Basisergänzungssatz''' <code>VECTSP_7:19</code>

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

===1.5.6.===
Mizar hat das Konzept von Anfang an allgemein aufgezogen.

===1.5.7.===
'''Beispiel''' <math>E_n</math> ist <code>1.(K,n)</code> (<code>MATRIX_1:def 3</code>).
# Multiplikation der <math>i</math>-ten Zeile mit <math>a</math> ist <code>ScalarXLine(A,i,a)</code> (<code>MATRIX12:def 2</code>)
# Addition der <math>j</math>-ten Zeile zur <math>i</math>-ten Zeile ist <code>RlineXScalar(A,i,j,1)</code> (<code>MATRIX12:def 3</code>)
# Addition des <math>a</math>-fachen der <math>j</math>-ten Zeile zur <math>i</math>-ten Zeile ist <code>RlineXScalar(A,i,j,a)</code> (<code>MATRIX12:def 3</code>)
# Vertauschen der <math>i</math>-ten mit der <math>j</math>-ten Zeile ist <code>InterchangeLine(A,i,j)</code> (<code>MATRIX12:def 1</code>)

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

'''Lemma''' z.T. <code>MATRIX15:69</code>, sonst keine Referenz

'''Satz''' keine explizite Referenz, aber s. <code>MATRIX15:sch 1,2</code>

'''Beispiel''' keine Referenz

===1.5.8.===
<math>^t A</math> ist <code>A@</code> (<code>MATRIX_0:def 6</code>); Rechenregeln: (1) <code>MATRIX_6:23</code> (2) nur reell: <code>MATRIXR1:30</code> (3) <code>MATRIX_0:57</code>

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

'''Lemma''' implizit über <code>MATRIX13:90,92</code> bzw. <code>MATRIX13:123</code>

===Aufgaben zu 1.5===
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz
# keine Referenz

==1.6 Summen von Vektorräumen==
===1.6.1.===
'''Definition''' Nur gegeben für die Summe zweier Vektorräume, <code>W1 + W2</code> (<code>VECTSP_5:def 1</code>), sonst keine Referenz.

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

'''Dimensionsformel für Summen''' <code>VECTSP_9:32</code>

===1.6.2.===
'''Lemma''' keine Referenz

'''Definition''' <math>V=W_1\oplus W_2</math> ist <code>V is_the_direct_sum_of W1, W2</code> (<code>VECTSP_5:def 4</code>).

===1.6.3.===
'''Satz''' (i => ii) implizit durch <code>VECTSP12:9</code> (i => iii) <code>VECTSP_5:def 4</code>, <code>VECTSP_9:34</code> (sonst) keine Referenz

'''Korollar''' <math>W'</math> ist <code>Linear_Compl of V</code> (<code>VECTSP_5:def 5</code>)

===1.6.4.===
'''Definition''' keine Referenz

'''Beispiel''' keine Referenz

'''Satz''' keine Referenz

===Aufgaben zu 1.6===
# keine Referenz
# keine Referenz
# ''<math>A</math> ist (schief)symmetrisch'' ist <code>A is (anti)symmetric</code> (<code>MATRIX_6:def 5,6</code>); keine Referenz für die Aufgaben