Mizarkommentare zu Gerd Fischers Lineare Algebra

Dieses Buch steht im Regal Mathematik.

Zusammenfassung des Projekts

„Mizarkommentare zu Gerd Fischers Lineare Algebra“ ist nach Einschätzung seiner Autoren zu 20 % fertig

Zielgruppe:

Deutschsprachige Mizarnutzer und solche, die es werden wollen.

Lernziele:

Verständnis, wo in der Mizar Mathematical Library (MML) Definitionen und Sätze der Linearen Algebra zu finden sind.

Buchpatenschaft/Ansprechperson:

Benutzer:Ayutac

Sind Co-Autoren gegenwärtig erwünscht?

Wenn jemand Deutsch spricht und sich mit Mizar auskennt (min. ein veröffentlichter Artikel), kann sich die Person gerne inhaltlich beteiligen. Da ich ein simples Referenzwerk schreibe, mag meine Formatierung aber möglicherweise zu wünschen übrig lassen

Richtlinien für Co-Autoren:

Ich halte meinen Stil für einfach kopierbar. Wichtig ist, dass wir NICHT das Buch "Lineare Algebra" von Gerd Fischer abtippen, sondern lediglich einen Referenzkatalog erstellen, was mit dem Urheberrecht völlig vereinbar sein sollte.

Projektumfang und Abgrenzung zu anderen Wikibooks:

Das deutschsprachige Wikibooks hat nichts Vergleichbares. Zuvor habe ich aber ein Analysisbuch auf dem englischsprachigen Wikibooks kommentiert.

Lizenzhinweis:

Für dieses Buch wurden zum Teil Sätze oder Passagen aus Mizar Commentary on Walter Rudin's Principles of Mathematical Analysis, welches unter einer CC BY-SA 3.0 Lizenz steht, sinngemäß oder wortwörtlich übersetzt.

Vorwort

Das Mizar-System besteht aus drei Teilen: einer formalen Sprache, um mathematische Beweise zu verfassen, ein Programm, um diese Beweise automatisiert auf Korrektheit zu prüfen und die Mizar Mathematical Library (kurz: MML; übersetzt: Mizar-Mathematikbibliothek). Seit ihrer Gründung 1989 ist die MML recht groß geworden und dies bringt ein kleines Problem mit sich:

F. Wiedijk: „The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward.“

Quelle: Writing a Mizar article in nine easy steps

Sinngemäße Übersetzung von Benutzer:Ayutac: "Die größte Herausforderung in Mizar zu schreiben besteht darin, das, was man braucht, in der MML zu finden, wobei MML die Abkürzung für die Mizar-Mathematikbibliothek ist. Leider hat dieses Problem keine einfache Lösung. Jeder wird aber feststellen, dass es abgesehen davon sehr simpel ist, einen Mizarartikel zu schreiben."

Dieses Buch ist der Versuch, dieses Problem zu überwinden. Es wurde das klassische Lineare-Algebra-Werk Lineare Algebra ("das Buch" innerhalb dieses Buches) von Gerd Fischer ausgewählt, um die darin enthaltenen Definitionen und Sätze (einschließlich Lemmata etc.) auf ihren entsprechenden Gegenstücke in der MML zu verweisen. Wo sich die mathematischen Konzepte zwischen dem Buch und der MML unterscheiden, wird dies wenn nötig erläutert. Beispielsweise erklärt das Buch nicht im Detail, was eine Relation ist, sondern führt zunächst Abbildungen ein und später Äquivalenzrelationen, während beide eine besondere Art von Relationen in Mizar sind.

Natürlich sind manche Definitionen oder Sätze nicht in der MML formalisiert, weil die MML einfach nicht die gesamte Mathematik beinhaltet. Zudem ist es, wie Wiedijk schrieb, nicht unbedingt einfach, eine bestimmte Aussage in der MML zu finden, die Autoren dieses Buches können trotz aller Anstrengung also auch etwas übersehen haben. Wenn also eine Aussage mit "keine Referenz" kommentiert ist, meint dies "keine Referenz gefunden".

Für dieses Buch wurde die 17. Auflage von Fischers Buch und Version 5.57.1363 der MML verwendet, wenn es nicht anders ausgezeichnet wurde.

Aufbau des Buches

Dieses Lehrwerk ist erst vor kurzem angelegt worden. – Nützliche Hinweise findest du im Wikibooks-Lehrbuch. – Bei Problemen kannst du unter diesem Link um Hilfe bitten. – Diskussionen zu diesem Buch führst du auf dieser Seite. – (Datum im Format Jahr_Monat_Tag: 20190922))

Details zu diesem Baustein erfährst du unter diesem Link.