Mathemagics

[Lean] Natural Number Game 2. Addition World

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..

부분집합(subset) 집합(set) \(A\)와 \(B\)에 대하여, \(B\)의 임의의 원소(element)가 \(A\)에 속하면(in) \(B\)는 \(A\)의 부분집합(subset)이라 하고 \(B \subseteq A\)로 표기한다. 특히, \(A \neq B\)이면서 \(B\)가 \(A\)의 부분집합인 경우 \(B \subset A\)로 표기한다. 진부분집합(proper subset)과 가부분집합(improper subset) 집합 \(A\)에 대하여, \(A\) 자신은 \(A\)의 가부분집합(improper subset)이다. \(A\)가 아닌 \(A\)의 부분집합은 진부분집합(proper subset)이다. 카테시안 곱(Cartesian product) 두 집합 \(A\), \(B\)에 대..