D110 · Matematika dalam Lean · Pilihan belajar dan mengajar
Pilih bagian, blok kode, dan latihan. Simpan rencana dengan ID sumber dan relasi solusi yang tetap utuh.
13 bab · 43 bagian · 243 unit bertanda latihan
Daftar bacaan lengkap — juga berfungsi tanpa JavaScript
- Memulai
- Ikhtisar
- Melakukan Perhitungan
- Membuktikan Identitas dalam Struktur Aljabar
- Menggunakan Teorema dan Lema
- Lebih Banyak Contoh Menggunakan apply dan rw
- Membuktikan Fakta tentang Struktur Aljabar
- Implikasi dan Kuantor Universal
- Kuantor Eksistensial
- Negasi
- Konjungsi dan Jika-dan-Hanya-Jika
- Disjungsi
- Barisan dan Konvergensi
- Himpunan
- Fungsi
- Teorema Schröder–Bernstein
- Akar Irasional
- Induksi dan Rekursi
- Bilangan Prima yang Tak Berhingga Banyaknya
- Induksi Lebih Lanjut
- Finset dan Fintype
- Argumen Pencacahan
- Tipe yang Didefinisikan secara Induktif
- Mendefinisikan Struktur
- Struktur Aljabar
- Membangun Bilangan Bulat Gauss
- Dasar-Dasar
- Morfisme
- Subobjek
- Monoid dan Grup
- Gelanggang
- Ruang vektor dan pemetaan linear
- Subruang dan ruang hasil bagi
- Endomorfisme
- Matriks, basis, dan dimensi
- Filter
- Ruang metrik
- Ruang topologi
- Kalkulus Diferensial Elementer
- Kalkulus Diferensial pada Ruang Bernorma
- Integrasi Elementer
- Teori Ukuran
- Integrasi
Susun pilihan Anda
Cakupan dan batas
- Bahasa Indonesia dan English tersedia untuk antarmuka, bacaan, dan cuplikan kode sumber. Ini bukan penulisan ulang dalam bahasa sehari-hari.
- Pembaca Inggris memakai revisi berbeda. Tautan bab/bagian memberi konteks bacaan, bukan bukti kesamaan setiap deklarasi kode.
- 243 unit ditandai sebagai latihan oleh sumber; beberapa merupakan contoh pengajaran. Enam tidak mempunyai relasi solusi tercatat.
- Solusi dapat mengisi satu lubang bukti atau memberi alternatif. Banyaknya solusi bukan banyaknya latihan yang selesai.
- Kode latihan dapat berupa satu blok bersama untuk beberapa ID. Nomor baris sumber bukan nomor baris terjemahan.
- Rencana memuat pilihan, asal sumber, dan tautan. Buku lengkap tidak disertakan untuk dibaca luring. Tidak ada kode Lean yang dijalankan.
Kode: Apache-2.0; teks buku: CC BY 4.0. Catatan komponen asli dipertahankan.
Data dan catatan sumber · Hasil pemeriksaan struktur