Mathemagics

[Lean] Natural Number Game 3. Multiplication World

Multiplication World에서는 Addition World에서 증명했던 Theorem들과, 곱셈에 관한 기본 Theorem들을 사용하여 곱셈의 교환법칙, 결합법칙, 그리고 분배법칙을 증명하고자 한다.Multiplication World Level 1Theorem mul_one: For any natural number \(m\), we have \(m \times 1=m\).theorem mul_one (m : ℕ) : m * 1 = m := byrw [one_eq_succ_zero]rw [mul_succ m 0]rw [mul_zero, zero_add]rflMultiplication World Level 2Theorem zero_mul: For all natural numbers \(m\),..

Lean과 Natural Number Game에 대한 간략한 소개는 이전 글에서 확인할 수 있다.Addition World에서는 덧셈의 교환법칙(add_comm)과 결합법칙(add_assoc)을 증명하는 것을 목표로 한다.지금까지의 과정에서 사용할 수 있는 Theorem은 add_zero, add_succ, succ_eq_add_one과, \(1=\text{succ} \ 0\), \(2=\text{succ} \ 1\)등의 자명한 equation이다.Addition World Level 1Theorem zero_add: For all natural numbers \(n\), we have \(0+n=n\).theorem zero_add (n : ℕ) : 0 + n = n := byinduction n w..

Lean은 프로그래밍 언어이자 증명보조기로 사용되는 도구이다.Natural Number Game을 통해, 인터랙티브 Lean을 사용하여 Lean의 문법을 간략히 학습할 수 있었다. 또한, 0을 포함한 (페아노 공리계를 따라 정의된) 자연수에서의 여러 Theorem을 순차적으로 증명하는 방법을 알 수 있었다. 다만, 인터랙티브인 만큼 증명이 긴 Theorem의 경우 가독성이 좋지 않기 때문에, indentation을 비롯한 추가적인 문법에 대해서는 추가로 알아둘 필요가 있을 것 같다.Tutorial World Level 1If \(x\) and \(q\) are arbitrary natural numbers, then \(37x+q=37x+q\).example (x q : ℕ) : 37 * x + q = ..

[5.3 Definition] 군의 위수(order) 군 \(G\)에 대하여, \(G\)의 위수 \(\vert G \vert \)(order \( \vert G \vert \) of \(G\))는 \(G\)의 원소의 수이다. [5.4 Definition] 부분군(subgroup) 군 \(G\)의 부분집합 \(H\)가 \(G\)의 이항연산에 대하여 닫혀 있으며, 집합 \(H\)와, \(G\)로부터 유도된 이항연산이 그 자체로도 군을 이룰 때, \(H\)는 \(G\)의 부분군(subgroup)이라 하고, \(H \leq G\) 또는 \(G \geq H\)라 한다. \(H \neq G\)인 경우 \(HH\)라 한다. 부분군의 예시 군 \(G\)에 대하여, 항등원이 \(e\)일 때, \(G\)와 \(\{e\}..

9. \(\langle U, \cdot \rangle\)은, \(\langle \mathbb{R}, + \rangle\)과 \(\langle \mathbb{R}^\ast, \cdot\rangle\) 둘 다와 동형이 아님을 보여라. \(\langle U, \cdot \rangle\)의 항등원은 \(1\), \(\langle \mathbb{R}, + \rangle\)의 항등원은 \(0\), \(\langle \mathbb{R}^\ast, \cdot\rangle\)의 항등원은 \(1\)이다. 이제 같은 원소를 3번 연산하여 항등원이 되는 원소, 즉 이항 구조 \(\langle S, \ast\rangle\)에 대하여 \(x \ast x \ast x =e\)의 해 \(x \in S\)의 개수를 구하자. 이때, 세..

[4.1 Definition] 군(group) 군(group)은 다음 조건을 만족하는 이항 구조 \(\langle G, \ast \rangle\)이다.\(\mathscr{G}_1\): 임의의 \(a, b, c \in G\)에 대하여, 결합 법칙 \[(a \ast b) \ast c = a \ast (b \ast c)\]이 성립한다. (associativity of \(\ast\))\(\mathscr{G}_2\): 임의의 \(x \in G\)에 대하여 \[e \ast x = x \ast e = x\]을 만족하는 항등원 \(e \in G\)가 존재한다. (identity element \(e\) for \(\ast\))\(\mathscr{G}_3\): 임의의 \(a \in G\) 각각에 대하여 \[a \ast..

이항 대수 구조(binary algebraic structure) 이항 대수 구조(binary algebraic structure) 은 집합 \(S\)와 그 위의 이항 연산 \(\ast\)을 통틀어 나타내며 \(\langle S, \ast \rangle\) 로 표기한다. 편의상 이항 구조(binary structure)로 쓰는 경우가 많다. [3.7 Definition] 동형사상(isomorphism)이항 대수 구조 \(\langle S, \ast \rangle\), \(\langle S', \ast' \rangle\)에 대하여, \(S\)와 \(S'\)의 동형사상(isomorphism)은 다음 조건(homomorphism property, 준동형 성질)을 만족하는 \(S\)에서 \(S'\)로의 일대일 ..

[2.1 Definition] 이항 연산(binary operation) 집합 \(S\) 위의 이항 연산(binary operation) \(\ast\)은 \(S \times S\)에서 \(S\)로의 함수이다. \((a, b) \in S \times S\)에 대하여, \(\ast((a, b)) \in S\)를 간단히 \(a \ast b\) 로 나타낸다.[2.3 Example] 집합 \(S\) 위의 이항 연산은 \(S \times S\)의 임의의 원소에 대하여 \(S\)의 한 원소를 매핑해야 한다. 따라서 실수 값을 갖는 행렬들의 집합 \(M(\mathbb{R})\) 위의 덧셈 \(+\)은 서로 다른 크기의 두 행렬 사이에서는 정의되지 않으므로 이항 연산이 아니다. [2.4 Definition] 닫혀 있음..

1. 서론 Spotify Web API는 Spotify에서 제공하는 콘텐츠에 대한 메타데이터를 추출할 수 있도록 도와주는 API입니다. Spotify Premium 사용자는 자신의 Dashboard에서 애플리케이션을 만들 수 있습니다. 이후 OAuth 2.0 방식을 사용하여 사용할 권한을 설정하고 권한 부여(authorization)를 하면, refresh token과 access token을 발급받을 수 있습니다. access token은 1시간(3,600초) 동안 유효한데, 이 access token이 만료된 경우 재발급에 refresh token을 사용합니다. access token은 앞으로 API를 활용한 호출(call)을 할 때마다 권한 확인을 위하여 header 부분에 들어가게 됩니다.2. 트..

복소수(complex numbers) 복소수(complex numbers) 집합 \(\mathbb{C}\) 는 \(\mathbb{C}=\{a+bi \vert a, b \in \mathbb{R}\}\)으로 정의된다. 이때, \(i\)는 \(i^2=-1\)을 만족하는 허수(imaginary number)이다. 오일러 공식(Euler's formula) 실수 \(\theta\)에 대하여, \(e^{i\theta}=\cos\theta+i\sin\theta\)가 성립한다. 임의의 실수 \(x\)에 대하여 \[e^x=1+x+\frac{x^2}{2!}+...+\frac{x^n}{n!}\]은 절대수렴한다. 따라서 항의 순서를 바꾼 \[e^x=\sum_{n=0}^{\infty} \frac{x^{2n}}{(2n)!}+\s..