Lean으로 배우는 수학

참고

이 문서는 Mathematics in Lean을 기계 번역 후 검토한 비공식 한국어 번역본입니다. 원문 텍스트는 CC BY 4.0에 따라 이용할 수 있으며, 이 문서에는 한국어 번역이라는 변경 사항이 적용되었습니다.

• 1. 소개
  • 1.1. 시작하기
  • 1.2. 개요
• 2. 기초
  • 2.1. 계산하기
  • 2.2. 대수적 구조에서 항등식 증명하기
  • 2.3. 정리와 보조정리 사용하기
  • 2.4. apply와 rw를 사용하는 추가 예제
  • 2.5. 대수적 구조에 관한 사실 증명하기
• 3. 논리
  • 3.1. 함의와 전칭 기호
  • 3.2. 존재 한정사
  • 3.3. 부정
  • 3.4. 논리곱과 필요충분조건
  • 3.5. 논리합
  • 3.6. 수열과 수렴
• 4. 집합과 함수
  • 4.1. 집합
  • 4.2. 함수
  • 4.3. 슈뢰더-베른슈타인 정리
• 5. 초등 정수론
  • 5.1. 무리수 근
  • 5.2. 귀납법과 재귀
  • 5.3. 소수는 무한히 많습니다
  • 5.4. 더 많은 귀납법
• 6. 이산수학
  • 6.1. Finset과 Fintype
  • 6.2. 개수 세기 논법
  • 6.3. 귀납적으로 정의된 타입
• 7. 구조체
  • 7.1. 구조체 정의
  • 7.2. 대수적 구조
  • 7.3. 가우스 정수 만들기
• 8. 계층 구조
  • 8.1. 기본 사항
  • 8.2. 사상(Morphisms)
  • 8.3. 부분 객체
• 9. 군과 환
  • 9.1. 모노이드와 군
  • 9.2. 환
• 10. 선형대수학
  • 10.1. 벡터 공간과 선형 사상
  • 10.2. 부분공간과 몫공간
  • 10.3. 자기사상
  • 10.4. 행렬, 기저와 차원
• 11. 위상수학
  • 11.1. 필터
  • 11.2. 거리 공간
  • 11.3. 위상 공간
• 12. 미분 계산법
  • 12.1. 초등 미분학
  • 12.2. 노름 공간에서의 미분법
• 13. 적분과 측도론
  • 13.1. 초등 적분
  • 13.2. 측도론
  • 13.3. 적분