From 38880b1f216ebb8706e72cbb658b4ea7f6cb4350 Mon Sep 17 00:00:00 2001 From: saundersp Date: Sun, 30 Mar 2025 22:05:09 +0200 Subject: [PATCH] Added proofs and fixed typos --- contents/algebra.tex | 214 +++++++++++++++----------- contents/dynamic_systems.tex | 80 +++++++++- contents/latex.tex | 26 ++++ contents/number_theory.tex | 128 ++++++++++------ contents/topology.tex | 1 + packages/lstlean.tex | 289 +++++++++++++++++++++++++++++++++++ packages/macros.sty | 15 +- packages/themes.sty | 31 +++- 8 files changed, 637 insertions(+), 147 deletions(-) create mode 100644 packages/lstlean.tex diff --git a/contents/algebra.tex b/contents/algebra.tex index cce08d0..c2d1273 100644 --- a/contents/algebra.tex +++ b/contents/algebra.tex @@ -10,10 +10,12 @@ Un magma est un ensemble $E$ avec une loi de composition interne $\function{\star}{E^2}{E}$ notée $(E, \star)$ tel que $\forall(a, b) \in E, a \star b \in E$. \end{definition_sq} +Typiquement, pour éviter d'inventer des nouvelles notations pour chaque loi de composition interne, on utilisera des notations déjà familières telles que \textbf{la notation additive (+)} directement héritée de l'addition des entiers naturels, ainsi que \textbf{la notation multiplicative ($\cartesianProduct$)}. + \langsubsection{Magma unital}{Unital magma} \begin{definition_sq} \label{definition:unital_magma} - Un magma \ref{definition:magma} $(E, \star)$ est dit \textbf{unital} si $\exists \Identity_E \in E, \forall a \in E, \Identity_E \star a = a \star \Identity_E = a$. + Un magma \ref{definition:magma} $(E, \star)$ est dit \textbf{unital} s'il existe un élément appelé \textbf{élément neutre} tel que si combiné avec n'importe quel élément ne le change pas, c'est-à-dire $$\exists \Identity_E \in E, \forall a \in E, \Identity_E \star a = a \star \Identity_E = a$$ \end{definition_sq} \begin{theorem_sq} @@ -106,11 +108,9 @@ $det\left(\begin{bmatrix}a & b\\c & d\end{bmatrix}\right) = ad - bc$ \langsubsubsection{Cas 3x3}{3x3 case} %TODO Complete subsubsection -\pagebreak - \subsection{Inverse} -\begin{theorem_sq} +\begin{theorem_sq} \label{theorem:matrix_product_monoid} Le tuple $(M_n(\K), \cartesianProduct)$ est un monoïde. \end{theorem_sq} @@ -132,17 +132,17 @@ $det\left(\begin{bmatrix}a & b\\c & d\end{bmatrix}\right) = ad - bc$ $MA = MB = \begin{pmatrix} -21 & -21 \\ 7 & 7 \end{pmatrix}$ alors que $M \ne 0 \land A \ne B$ \end{proof} -% \begin{theorem_sq} -% $\lnot(\forall (A, B) \in M_n(\K)^2, AB = 0 \implies A = 0 \lor B = 0)$ -% \end{theorem_sq} +\begin{theorem_sq} + $\lnot(\forall (A, B) \in M_n(\K)^2, AB = 0 \implies A = 0 \lor B = 0)$ +\end{theorem_sq} -% \begin{proof} -% Soit $(A, B) \in M^*_2(\K)^2$ tel que -% -% $A := \begin{pmatrix} 3 & -12 \\ -2 & 8 \end{pmatrix}$ \hspace{5mm} $B := \begin{pmatrix} 4 & 12 \\ 1 & 3 \end{pmatrix}$ -% -% $AB = 0$ alors que $A \ne 0 \land B \ne 0$ -% \end{proof} +\begin{proof} + Soit $(A, B) \in M^*_2(\K)^2$ tel que + + $A := \begin{pmatrix} 3 & -12 \\ -2 & 8 \end{pmatrix}$ \hspace{5mm} $B := \begin{pmatrix} 4 & 12 \\ 1 & 3 \end{pmatrix}$ + + $AB = 0_2$ alors que $A \ne 0 \land B \ne 0$ +\end{proof} \begin{definition_sq} \label{definition:inversible_matrix} Une matrice $A \in M_n(\K)$ est dite \textbf{inversible} sur $\K$ si et seulement s'il existe une matrice dite \textbf{inverse} $B \in M_n(\K)$ tel que $AB = \Identity_n = BA$. @@ -156,25 +156,27 @@ $det\left(\begin{bmatrix}a & b\\c & d\end{bmatrix}\right) = ad - bc$ - Les matrices de dilatation $D_i(a)$ sont inversibles : $(D_i(a))^{-1} = D_i(a^{-1})$ -- Les matrices de permutation $P_{i, j}$ sont inversibles : $(P_{i, j})^{-1} = P_{i, j}$ +- Les matrices de permutation $P_{i, j}$ sont inversibles : $(P_{i, j})^{-1} = P_{j, i}$ \begin{definition_sq} \label{definition:linear_group} L'ensemble des matrices inversibles est appelé \textbf{groupe linéaire} et est noté $GL_n(\K)$. - - Également, le tuple $(GL_n(\K), \cartesianProduct)$ est un groupe \ref{definition:group}. \end{definition_sq} -Par la théorie des groupes : +\begin{theorem_sq} + Le tuple $(GL_n(\K), \cartesianProduct)$ est un groupe \ref{definition:group}. +\end{theorem_sq} -\begin{itemize} - \item{L'inverse est unique : $AB = AC = \Identity_n \implies B = C = A^{-1}$} - \item{L'inverse d'un inverse est l'identité : $(A^{-1})^{-1} = A$} - \item{Le produit de deux matrices inversibles est inversible : $(AB)^{-1} = B^{-1}A^{-1}$} -\end{itemize} +\begin{proof} + L'ensemble des matrices inversibles sont également des matrices, donc $GL_n(\K) \subseteq M_n(\K)$ or le tuple $(M_n(\K), \cartesianProduct)$ est un monoïde \ref{theorem:matrix_product_monoid} et $GL_n(\K)$ ne garde que les matrices qui sont inversibles et cela constitue la définition d'un groupe \ref{definition:group}. +\end{proof} -La transposée d'un inverse et l'inverse de la transposée : $(A^{-1})^T = (A^T)^{-1}$ +\begin{theorem_sq} + La transposée d'un inverse et l'inverse de la transposée c.-à-d. : $\forall A \in GL_n(\K), (A^{-1})^T = (A^T)^{-1}$ +\end{theorem_sq} -$(A^{-1})^T A^T = (AA^{-1})^T = \Identity_n^T = \Identity_n$ et $A^T(A^{-1})^T = (A^{-1}A)^T = \Identity_n^T = \Identity_n$ +\begin{proof} + $\forall A \in GL_n(\K), (A^{-1})^T A^T = (AA^{-1})^T = \Identity_n^T = \Identity_n \land A^T(A^{-1})^T = (A^{-1}A)^T = \Identity_n^T = \Identity_n$ +\end{proof} \begin{theorem_sq} $\forall (A, B) \in M_n(\K)^2, \forall M \in GL_n(\K), (MA = MB) \equivalence A = B$ @@ -195,14 +197,19 @@ $(A^{-1})^T A^T = (AA^{-1})^T = \Identity_n^T = \Identity_n$ et $A^T(A^{-1})^T = \begin{proof} Par récurrence sur $n$. Le cas d'initialisation $n = 1$ est immédiat. - Passons à l'hérédité. Soit $A \in GL_n(\K)$ avec $n \ge 2$ et supposons l'hypothèse $h$ au rang $n - 1$. On va appliquer l'algorithme du pivot de Gauss. - Comme A est inversible, sa première colonne n'est pas nulle. - Si $a_{11} \ne 1$, alors il existe $i > 1$ tel que la matrice de transvection $T_{1, i}(\frac{1 - a_{11}}{a_{i1}})$ (ou l'opération $L_1 \leftarrow L_1 + \frac{1 - a_{11}}{a_{i1}}L_i$) permet de mettre un coefficient 1 en position $(1, 1)$. + Passons à l'hérédité. Soit $A \in GL_n(\K)$ avec $n \ge 2$ et supposons l'hypothèse $h$ au rang $n - 1$. + Appliquons l'algorithme du pivot de Gauss. + Comme A est inversible, sa première colonne est nécessairement non nulle. + + Si $a_{11} \ne 1$, s'il existe $i > 1$ tel que la matrice de transvection $T_{1, i}(\frac{1 - a_{11}}{a_{i1}})$ permet de mettre un coefficient 1 en position $(1, 1)$. + + Dans le cas ou $a_{11} \ne 1$ et qu'il s'agit du seul coefficient non nul de la colonne, nous pouvons ajouter la matrice de transvection $T_{2, 1}(1)$ pour nous ramener au cas précédent. + Ensuite, en utilisant le coefficient $(1, 1)$ comme pivot, une succession d'opérations sur les lignes puis sur les - colonnes permet d'annuler tous les autres coefficients de la première ligne et de la première colonne : il existe - des matrices de transvection cela permet d'affirmer qu'il existe une suite finie de matrices de transvection $M_k$ telles que + colonnes permet d'annuler tous les autres coefficients de la première ligne et de la première colonne, cela permet d'affirmer qu'il existe une suite finie de matrices de transvection $M_k$ telles que $A \prod\limits_{i = 1}^k M_i = \begin{pmatrix} 1 & 0 \\ 0 & A' \end{pmatrix}$ - où $A' \in GL_{n - 1}(\K)$ ainsi que $\det(A') = \det(A)$, avec l'hypothèse $h$ on conclut l'hérédité. + où $A' \in GL_{n - 1}(\K)$ ainsi que $\det(A') = \det(A)$. + En appliquant l'hypothèse $h$ on conclut l'hérédité. \end{proof} \begin{theorem_sq} @@ -225,48 +232,74 @@ $(A^{-1})^T A^T = (AA^{-1})^T = \Identity_n^T = \Identity_n$ et $A^T(A^{-1})^T = Supposons que la matrice $A$ est inversible, c'est-à-dire qu'il existe une matrice $A^{-1}$ telle que $AA^{-1} = A^{-1}A = \Identity_n$. - % TODO Fix proof... - Alors, $\rank{A} = n$. + % \Limpliespart - En effet, si $\rank{A} = n$, ainsi, il existe une matrice colonne de taille $n$ qui est un multiple scalaire des colonnes de $A$, ce qui signifie que les vecteurs colonnes de $A$ sont linéairement indépendants. + % Supposons que $\rank{A} = n$. + % Sachant que les matrices de dilatation et transvection conservent le rang, et que la matrice identité $\Identity_n$ à un rang de $n$ + % alors, nous pouvons créer une séquence finie de $k$ matrices de dilatation et de transvection tel que $A = \prod\limits_{i = 1}^k E_i$. + % Hors comme toutes les matrices de dilation te de transvection sont inversibles ainsi que leur produit, ainsi, nous pouvons créer une autre séquence finie $B = \prod\limits_{i = 1}^k (E_{k - i - 1})^{-1}$. - \Limpliespart + % On remarque de $AB = \left(\prod\limits_{i = 1}^k E_i\right) \left(\prod\limits_{i = 1}^k (E_{k - i - 1})^{-1}\right) = \prod\limits_{i = 1}^k \Identity_n = \Identity_n$. - Supposons que $\rank{A} = n$. - Sachant que les matrices de dilatation et transvection conservent le rang, et que la matrice identité $\Identity_n$ à un rang de $n$ - alors, nous pouvons créer une séquence finie de $k$ matrices de dilatation et de transvection tel que $A = \prod\limits_{i = 1}^k E_i$. - Hors comme toutes les matrices de dilation te de transvection sont inversibles ainsi que leur produit, ainsi, nous pouvons créer une autre séquence finie $B = \prod\limits_{i = 1}^k (E_{k - i - 1})^{-1}$. - - On remarque de $AB = \left(\prod\limits_{i = 1}^k E_i\right) \left(\prod\limits_{i = 1}^k (E_{k - i - 1})^{-1}\right) = \prod\limits_{i = 1}^k \Identity_n = \Identity_n$. - - Donc, non seulement $A$ est inversible, mais avons aussi un algorithme qui permet de calculer sa matrice inverse. + % Donc, non seulement $A$ est inversible, mais avons aussi un algorithme qui permet de calculer sa matrice inverse. % TODO Fix garbage AI proof... -Dans cet article, nous prouvons que si le rang d'une matrice $A$ est égal à son ordre (taille), -alors la matrice $A$ est inversible en utilisant des matrices élémentaires. +% Dans cet article, nous prouvons que si le rang d'une matrice $A$ est égal à son ordre (taille), +% alors la matrice $A$ est inversible en utilisant des matrices élémentaires. +% +% Supposons que la matrice $A \in M_n(\K)$ et que $\rank{A} = n$. +% +% Montrer qu'il existe une matrice inversible composée de matrices élémentaires. +% +% Supposons que $A$ est une matrice de taille $n$ avec $\rank{A} = n$. +% Nous savons que pour toute opération sur les lignes (ou les colonnes), +% la matrice résultante aura un rang égal ou inférieur à la matrice originale $A$. +% Par conséquent, nous pouvons effectuer une séquence d'opérations élémentaires sur les lignes de $A$ sans changer son rang. +% +% Soit $E_1, E_2, \ldots, E_k$ ces matrices élémentaires telles que leur produit est également une matrice élémentaire. Nous avons $A = \prod\limits_{i = 1}^n E_i$ +% +% Puisque $\rank{A} = n$, et que chaque $E_i$ maintient le rang, il s'ensuit que toutes ces matrices sont des matrices élémentaires avec un élément pivot non nul (elles ne peuvent pas être la matrice zéro). +% On peut donc construire une matrice inversible composée uniquement de ces matrices élémentaires : +% \[ B = E_1(E_2(\cdots E_k(I_n))\cdots) \] +% Cette matrice $B$ est clairement inversible puisqu'elle a un pivot non nul dans chaque ligne (ou colonne), et donc son rang est égal à l'ordre de la matrice originale $A$. +% Ainsi, nous avons montré que si $\rank{A} = n$, il existe une matrice inversible composée uniquement de matrices élémentaires. -Supposons que la matrice $A \in M_n(\K)$ et que $\rank{A} = n$. +Ok -Montrer qu'il existe une matrice inversible composée de matrices élémentaires. +Ok -Supposons que $A$ est une matrice de taille $n$ avec $\rank{A} = n$. -Nous savons que pour toute opération sur les lignes (ou les colonnes), -la matrice résultante aura un rang égal ou inférieur à la matrice originale $A$. -Par conséquent, nous pouvons effectuer une séquence d'opérations élémentaires sur les lignes de $A$ sans changer son rang. +Ok -Soit $E_1, E_2, \ldots, E_k$ ces matrices élémentaires telles que leur produit est également une matrice élémentaire. Nous avons $A = \prod\limits_{i = 1}^n E_i$ + \impliespart +Since $AA^{-1} = I_n$, the columns of $A$ must be linearly independent. -Puisque $\rank{A} = n$, et que chaque $E_i$ maintient le rang, il s'ensuit que toutes ces matrices sont des matrices élémentaires avec un élément pivot non nul (elles ne peuvent pas être la matrice zéro). -On peut donc construire une matrice inversible composée uniquement de ces matrices élémentaires : -\[ B = E_1(E_2(\cdots E_k(I_n))\cdots) \] -Cette matrice $B$ est clairement inversible puisqu'elle a un pivot non nul dans chaque ligne (ou colonne), et donc son rang est égal à l'ordre de la matrice originale $A$. -Ainsi, nous avons montré que si $\rank{A} = n$, il existe une matrice inversible composée uniquement de matrices élémentaires. +To see this, suppose the columns of $A$ are linearly dependent. Then there exist scalars $c_1, c_2, ..., c_n$, not all zero, such that +$$c_1 \mathbf{a}_1 + c_2 \mathbf{a}_2 + \dots + c_n \mathbf{a}_n = \mathbf{0}$$ +where $\mathbf{a}_i$ are the columns of $A$. This can be written as $A\mathbf{c} = \mathbf{0}$, where $\mathbf{c} = \begin{bmatrix} c_1 \\ c_2 \\ \vdots \\ c_n \end{bmatrix}$ is a non-zero vector. + +If $A$ is invertible, then we can multiply both sides by $A^{-1}$: +$$A^{-1}A\mathbf{c} = A^{-1}\mathbf{0} \implies \mathbf{c} = \mathbf{0}$$ +But this contradicts our assumption that $\mathbf{c}$ is a non-zero vector. Therefore, the columns of $A$ must be linearly independent. + +Since $A$ is an $n \times n$ matrix with $n$ linearly independent columns, the column space of $A$ has dimension $n$. Therefore, rank$(A) = n$. + + \Limpliespart + + $\rank{A} = n$ implies that $A$ is an $n \times n$ matrix with $n$ linearly independent rows. +Since the columns of $A$ are linearly independent and span $\K^n$, any vector $\mathbf{b} \in \K^n$ can be written as a linear combination of the columns of $A$. In other words, for any $\mathbf{b} \in \K^n$, the equation $A\mathbf{x} = \mathbf{b}$ has a solution. Since the columns are linearly independent, the solution is unique. + +Consider the system $A\mathbf{x} = \mathbf{e}_i$, where $\mathbf{e}_i$ is the $i$-th standard basis vector in $\K^n$ (i.e., a vector with a 1 in the $i$-th position and 0s elsewhere). Since rank$(A) = n$, this system has a unique solution for each $i = 1, 2, ..., n$. Let $\mathbf{x}_i$ be the unique solution to $A\mathbf{x} = \mathbf{e}_i$. + +Now, construct a matrix $B$ whose columns are the vectors $\mathbf{x}_1, \mathbf{x}_2, ..., \mathbf{x}_n$. Then $AB$ is a matrix whose $i$-th column is $A\mathbf{x}_i = \mathbf{e}_i$. Therefore, $AB = I_n$. + +Since $AB = I_n$, we have shown that $A$ has a right inverse. For square matrices, if a right inverse exists, then it is also a left inverse. Therefore, $BA = I_n$ as well. Thus, $B = A^{-1}$, and $A$ is invertible. \end{proof} \begin{definition_sq} \label{definition:special_linear_group} - L'ensemble \textbf{groupe spécial linéaire} noté $SL_n(\K)$ est le sous ensemble de $GL_n(\K)$ tel que le déterminant est égale à 1. + L'ensemble \textbf{groupe spécial linéaire} noté $SL_n(\K)$ est le sous ensemble de $GL_n(\K)$ tel que le déterminant est égale à 1, c'est-à-dire + $$SL_n(\K) := \{ A \in GL_n(\K) \suchthat \det(A) = 1\}$$ \end{definition_sq} \begin{theorem_sq} @@ -274,11 +307,17 @@ Ainsi, nous avons montré que si $\rank{A} = n$, il existe une matrice inversibl \end{theorem_sq} \begin{proof} - Vérifions chaque axiome d'un groupe. $\det(\Identity_n) = 1 \equivalence \Identity_n \in SL_n(\K)$. + Grâce aux propriétés du déterminant, on peut vérifier chaque axiome d'un sous-groupe \ref{definition:subgroup} - La propriété du déterminant $\forall (A, B) \in M_n(\K)^2, \det(AB) = \det(A)\det(B)$ permet de montrer les propositions suivantes : - $$\forall (A, B) \in SL_n(\K)^2, \det(AB) = \det(A)\det(B) = 1 * 1 = 1 \implies AB \in SL_n(\K)$$ - $$\forall A \in SL_n(\K), \exists! A^{-1} \in GL_n(\K), 1 = \det(\Identity_n) = \det(AA^{-1}) = \det(A)\det(A^{-1}) = \det(A^{-1}) \implies A^{-1} \in SL_n(\K)$$ + \begin{itemize} + \item{Magma : $\forall (A, B) \in SL_n(\K)^2, \det(AB) = \det(A)\det(B) = 1 \cdot 1 = 1 \implies AB \in SL_n(\K)$} + \item{Présence de l'identité : $\det(\Identity_n) = 1 \implies \Identity_n \in SL_n(\K)$} + \item{Présence de l'inverse : $\forall A \in SL_n(\K), \exists! A^{-1} \in GL_n(\K), 1 = \det(\Identity_n) = \det(AA^{-1}) = \det(A)\det(A^{-1}) = \det(A^{-1}) \implies A^{-1} \in SL_n(\K)$} + \end{itemize} + + Pour montrer qu'il s'agit d'un sous-groupe distingué, posons $x \in GL_n(\K)$ et $y \in SL_n(\K)$, nous pouvons en conclure + + $\det(xyx^{-1}) = \det(x)\det(y)\det(x)^{-1} = 1 \implies xyx^{-1} \in SL_n(\K)$ \end{proof} \begin{theorem_sq} @@ -290,13 +329,12 @@ Ainsi, nous avons montré que si $\rank{A} = n$, il existe une matrice inversibl $$A \prod\limits_{i = 1}^p M_i = \Identity_n$$ \end{proof} -\pagebreak - \begin{theorem_sq} Une matrice $A \in M_n(\K)$ est inversible sur $\K$ si et seulement si $det(A) \neq 0$. \end{theorem_sq} \begin{proof} + \lipsum[2] % TODO Complete proof \end{proof} @@ -332,7 +370,7 @@ $a \in Tr_n$ \begin{proof} Soit $A \in M_n(\K)$ ainsi qu'une norme subordonnée quelconque $\matrixnorm{.}$. - $$\forall n \in \N, \matrixnorm{\frac{A^n}{n!}} \le \frac{\matrixnorm{A^n}}{n!}$$ + $$\forall n \in \N, \left\lVert \frac{A^n}{n!} \right\rVert \le \frac{\matrixnorm{A^n}}{n!}$$ \end{proof} \begin{theorem_sq} @@ -388,36 +426,34 @@ $a \in Tr_n$ Les deux formules de polarisation s'en déduisent immédiatement. \end{proof} -\langsection{Espaces vectoriels}{Vectors spaces} \label{definition:vector_space} -%TODO Complete section +\langsection{Espaces vectoriels}{Vectors spaces} -Soit $(E, +)$ un groupe abélien \ref{definition:abelian_group} de $\K$ +\begin{definition_sq} \label{definition:vector_space} + Un espace vectoriel $(E(\K), +, \cartesianProduct)$ sur un corps $\K$ est un tuple + Soit $(E, +)$ un groupe abélien \ref{definition:abelian_group} de $\K$ -\begin{itemize} - \item{muni d'une loi de composition externe d'un corps $\K$ tel que $\function{(\cdot)}{K \cartesianProduct E}{E}$ vérifiant $(\alpha, x) \rightarrow \alpha x$} -\end{itemize} + \begin{itemize} + \item{muni d'une loi de composition externe d'un corps $\K$ tel que $\function{(\cdot)}{K \cartesianProduct E}{E}$ vérifiant $(\alpha, x) \rightarrow \alpha x$} + \end{itemize} -\bigskip -Et vérifiant $\forall(\alpha, \beta) \in \K^2, \forall(a, b, c) \in E^3$ + \bigskip + Et vérifiant $\forall(\alpha, \beta) \in \K^2, \forall(a, b, c) \in E^3$ -\begin{itemize} - \item{Unital en $(\cdot)$} - \item{Distributivité (gauche et droite) $+$ de $\K \equivalence a(\alpha + \beta) = (\alpha + \beta)a = \alpha a + \beta a$} - \item{Distributivité (gauche et droite) $*$ de $\K \equivalence a(\alpha * \beta) = (\alpha * \beta)a = \alpha(\beta a)$} -\end{itemize} - -\langsubsection{Famille libre}{Free family} \label{definition:vector_space_free_family} - -\begin{definition_sq} -Une famille \suite{e} est dite \textbf{libre} si -$$\forall i \in \discreteInterval{1, n}, \lambda_i \in \K, \sum\limits_{i = 1}^n \lambda_i e_i = 0 \implies \lambda_i = 0$$ + \begin{itemize} + \item{Unital en $(\cdot)$} + \item{Distributivité (gauche et droite) $+$ de $\K \equivalence a(\alpha + \beta) = (\alpha + \beta)a = \alpha a + \beta a$} + \item{Distributivité (gauche et droite) $*$ de $\K \equivalence a(\alpha * \beta) = (\alpha * \beta)a = \alpha(\beta a)$} + \end{itemize} \end{definition_sq} -\langsubsection{Famille génératrice}{Generating family} \label{definition:vector_space_generating_family} +\begin{definition_sq} \label{definition:vector_space_free_family} + Une famille \suite{e} est dite \textbf{libre} si la seule combinaison linéaire qui annule \suite{e} est la combinaison linéaire nulle, c'est-à-dire + $$\forall \lambda \in \K^n, \sum\limits_{i = 1}^n \lambda_i e_i = 0 \implies \lambda_i = 0$$ +\end{definition_sq} -\begin{definition_sq} -Une famille \suite{e} est dite \textbf{génératrice} de $E$ si -$$\forall v \in E, \exists \lambda \in \K^n, \sum\limits_{i=1}^n \lambda_i e_i = v$$ +\begin{definition_sq} \label{definition:vector_space_generating_family} + Une famille \suite{e} est dite \textbf{génératrice} d'un espace vectoriel \ref{definition:vector_space} $E$ si pour tout vecteur $v$ de $E$ il existe une combinaison linéaire de \suite{e} égale à $v$, c'est-à-dire + $$\forall v \in E, \exists \lambda \in \K^n, \sum\limits_{i=1}^n \lambda_i e_i = v$$ \end{definition_sq} \langsubsection{Bases}{Basis} \label{definition:vector_space_basis} @@ -484,7 +520,7 @@ $\implies F \subset G \lor G \subset F$ \langsubsection{Application linéaire}{Linear map} \label{definition:linearity} -\begin{definition_sq} \label{defintion:linear_map} +\begin{definition_sq} \label{definition:linear_map} Une application $\function{f}{\K}{\K}$ est une \textbf{application linéaire} d'un $\K$-espace vectoriel $E$ si il respecte les axiomes suivants : \begin{itemize} \item{\lang{Additivité}{Additivity} : $\forall(x, y) \in E^2, f(x + y) = f(x) + f(y)$} diff --git a/contents/dynamic_systems.tex b/contents/dynamic_systems.tex index dcbb47a..be73d4f 100644 --- a/contents/dynamic_systems.tex +++ b/contents/dynamic_systems.tex @@ -1,9 +1,61 @@ \pagebreak + +%\documentclass{article} + +%\usepackage{paracol} \columnratio{0.5} +% Défini la longueur des marges du document (défault à 4.8cm) +%\usepackage[margin=2.5cm]{geometry} + +%\usepackage{xcolor} +% mode sombre +%\definecolor{colour_bg} {HTML} {222324} +%\definecolor{colour_fg} {HTML} {FFFFFF} +% mode par défaut +% \definecolor{colour_bg} {RGB} {255, 255, 255} +% \definecolor{colour_fg} {RGB} {0, 0, 0} +% \pagecolor{colour_bg} +% \color{colour_fg} +% \usepackage{mdframed} +% \mdfsetup{linecolor = colour_fg, innerlinecolor = colour_fg, middlelinecolor = colour_fg, outerlinecolor = colour_fg, % +% backgroundcolor = colour_bg, fontcolor = colour_fg} + +% Include missing symbols s.a "Natural Numbers" +% \usepackage{amsfonts} +%\usepackage{amssymb} % for '\blacksquare' macro +% \usepackage{amsthm} % for 'proof' environment +% \usepackage{mathtools} + +% \newcommand{\function}[3]{#1 \colon #2 \longrightarrow #3} +% \newcommand{\functiondef}[2]{\hspace{15pt}#1 \longmapsto #2} +% \DeclareMathOperator{\composes}{\circ} % New symbol composing morphisms +% \newcommand{\suchthat}{\mid} +% \newcommand{\discreteInterval}[1]{[\![#1]\!]} +% \newcommand{\N}{\mathbb{N}} % Natural numbers symbol +% \newcommand{\R}{\mathbb{R}} % Real numbers symbol +% \DeclarePairedDelimiter{\abs}{|}{|} +% \DeclarePairedDelimiter{\norm}{\lVert}{\rVert} +% \DeclareMathOperator{\intersection}{\cap} + +% \newtheorem{definition}{Définition} +% \newenvironment{definition_sq}[1][]{\begin{mdframed}\begin{definition}[#1]}{\end{definition}\end{mdframed}} +% \newtheorem{theorem}{Théorème} +% \newenvironment{theorem_sq}[1][]{\begin{mdframed}\begin{theorem}[#1]}{\end{theorem}\end{mdframed}} + +% Manière classique de créer le titre avec la commande maketitle +% \title{Introduction aux systèmes dynamiques} +% \author{Pierre Saunders, William De Canteloube} +% \date{L3 Maths 2024-2025, Université Côte d'Azûr} + +%\begin{document} + +%\maketitle + \begin{paracol}{2} Pierre Saunders +William De Canteloube \switchcolumn \begin{flushright} L3 Math 2024-25 @@ -37,7 +89,25 @@ Pour l'instant, nous nous intéresserons à la fonction suivante : $$\function{T_b}{[0, 1]}{[0, 1]}$$ $$\functiondef{x}{b x \mod 1}$$ -Par induction sur le nombre d'applications successives $n$ on trouve immédiatement que $T_b^n = b^n x \mod 1$. En écrivant $x \in [0, 1]$ en écriture décimale en base $b$ i.e. +\begin{prop_sq} + $\forall x \in [0, 1], T_b^n(x) = b^n x \mod 1$. +\end{prop_sq} + +\begin{proof} + Soit $x \in [0, 1]$, procédons par induction sur le nombre d'applications successives $n$, la définition de la fonction $T_b$ est le cas initial à $n = 1$. + Supposons l'hypothèse vraie pour un rang $n$ et prouvons l'hérédité $n + 1$. + $$T_b^n(x) = b^n x \mod 1 \implies T_b \composes T_b^n(x) = b(b^n x) \mod 1 = b^{n + 1} x \mod 1 = T_b^{n + 1}(x)$$ +\end{proof} + +\begin{prop_sq} \label{prop:repeating_composition} + Le nombre de points périodiques de longueur $n$ de la fonction $T_b$ est égal à $b^n - 1$. +\end{prop_sq} + +\begin{proof} + Soit $x \in [0, 1]$ un point périodique de longueur $n \implies T_b^n (x) = x$ or par \ref{prop:repeating_composition} $b^n x = x$ +\end{proof} + +En écrivant $x \in [0, 1]$ en écriture décimale en base $b$ i.e. $$x = \sum\limits_{i = 0}^{+\infty} \frac{d_i}{b^{i + 1}} = 0. d_0 d_1 d_2 \cdots d_m \cdots$$ @@ -76,6 +146,12 @@ Cela est équivalent à glisser les décimales vers la gauche. Donc pour étudie \end{proof} \begin{definition_sq} - Un endomorphisme continue d'un espace topologique $(E, \tau_E)$ est dit \textbf{topologiquement transitif} si pour toute paire d'ouverts non-vide $U, V \subseteq E$ il existe $n \in \N$ tel que $f^n(U) \intersection V \ne \emptyset$. + Un endomorphisme $f$ d'un espace topologique $(E, \tau_E)$ est dit \textbf{topologiquement transitif} si pour toute paire d'ouverts non-vide $U, V \subseteq E$ il existe $n \in \N$ tel que $f^n(U) \intersection V \ne \emptyset$. \end{definition_sq} +ANNEXE + +TODO : Theorem x in Q iff x has repeating decimals %\label{theorem:repeating_decimals} + +%\end{document} + diff --git a/contents/latex.tex b/contents/latex.tex index 5cd620f..329ce4e 100644 --- a/contents/latex.tex +++ b/contents/latex.tex @@ -97,6 +97,32 @@ \end{itemize} \end{mdframed} +\langsection{Tableau}{Table} + +\begin{verbatim} + \begin{tabular}{|c|c|c|} + \hline + $C_{1, 1}$ & $C_{2, 1}$ & $C_{3, 1}$ \\ + \hline + $C_{1, 2}$ & $C_{2, 2}$ & $C_{3, 2}$ \\ + \hline + $C_{1, 3}$ & $C_{2, 3}$ & $C_{3, 3}$ \\ + \hline + \end{tabular} +\end{verbatim} + +\begin{mdframed} + \begin{tabular}{|c|c|c|} + \hline + $C_{1, 1}$ & $C_{2, 1}$ & $C_{3, 1}$ \\ + \hline + $C_{1, 2}$ & $C_{2, 2}$ & $C_{3, 2}$ \\ + \hline + $C_{1, 3}$ & $C_{2, 3}$ & $C_{3, 3}$ \\ + \hline + \end{tabular} +\end{mdframed} + \langsection{Paquets additionnels}{Additional packages} %TODO Complete section diff --git a/contents/number_theory.tex b/contents/number_theory.tex index 3bcba35..577b0f4 100644 --- a/contents/number_theory.tex +++ b/contents/number_theory.tex @@ -126,6 +126,53 @@ $\functiondef{n}{\begin{cases}n \le 0 & -2n \\ \otherwise & 2n-1 \end{cases}}$ \end{proof} +\begin{theorem_sq} + Tous les entiers relatifs sont soit pairs ou impairs. +\end{theorem_sq} + +\begin{proof} + Procédons par induction. L'initialisation $n = 0$ est directe, car $2 \cdot 0 = 0$ ce qui montre que $0$ est pair. +\end{proof} + +% \begin{leancode} +\begin{lstlisting}[language=lean] +theorem every_integer_is_even_or_odd (n : ℤ) : Even n ∨ Odd n := by + induction n with + | hz => + left + use 0 + group + | hp n' hz => + cases hz with + | inl hl => + right + obtain ⟨a, ha⟩ := hl + rw [ha] + use a + group + | inr hr => + left + obtain ⟨a, ha⟩ := hr + rw [ha] + use a + 1 + group + | hn n' hz => + cases hz with + | inl hl => + right + obtain ⟨a, ha⟩ := hl + rw [ha] + use a - 1 + group + | inr hr => + left + obtain ⟨a, ha⟩ := hr + rw [ha] + use a + group +\end{lstlisting} +% \end{leancode} + \langsection{Construction des rationnels $(\Q)$}{Construction of rational numbers} %TODO Complete section @@ -136,7 +183,7 @@ $\Q := (p,q) = \Z \cartesianProduct \N^*$ \langsubsection{Relations binaries}{Binary relations} %TODO Complete subsection -$\forall (p,q) \in \Q, \forall n \in \N^*, \frac{p}{q} \equivalence \frac{p \cdot n}{q \cdot n}$ +$\forall (p,q) \in \Q, \forall n \in \Z^*, \frac{p}{q} \equivalence \frac{p \cdot n}{q \cdot n}$ \langsubsection{Opérateurs}{Operators} %TODO Complete subsection @@ -254,7 +301,7 @@ Lors d'une longue division, on effectue l'opération $r = p \mod{q}$, par défin \langsubsection{Construction de Cayley–Dickson}{Cayley–Dickson's construction} -Source: \citeannexes{wikipedia_cayley_dickson} +Source : \citeannexes{wikipedia_cayley_dickson} \langsubsection{Coupes de Dedekind}{Dedekind's cuts} %TODO Complete subsection @@ -262,7 +309,7 @@ Source: \citeannexes{wikipedia_cayley_dickson} \langsection{Construction des complexes $(\C)$}{Construction of complex numbers} %TODO Complete section -Source: \citeannexes{wikipedia_complex_number} +Source : \citeannexes{wikipedia_complex_number} $\C = (a,b) \in R, a + ib ~= \R $ @@ -304,7 +351,7 @@ $\forall((a,b),(c,d)) \in \C, a + ib \Rel_L c + id := \begin{cases} \section{Construction des quaternions $(\Hq)$} -Source: \citeannexes{wikipedia_quaternion} +Source : \citeannexes{wikipedia_quaternion} \langsubsection{Table de Cayley}{Cayley's table} %TODO Complete subsection @@ -326,7 +373,7 @@ Source: \citeannexes{wikipedia_quaternion} \section{Construction des octonions $(\Ot)$} -Source: \citeannexes{wikipedia_octonion} +Source : \citeannexes{wikipedia_octonion} \langsubsection{Table de Cayley}{Cayley's table} %TODO Complete subsection @@ -362,9 +409,9 @@ $e_ie_j = \begin{cases} e_j, & \text{if i = 0} \\ e_i, & \text{if j = 0} \\ -\de Où $\delta_{ij}$ est le symbole de Kronecker et $\epsilon_{ijk}$ est un tenseur complètement anti-symétrique. -\section{Construction des sedenions $(\Se)$} +\langsection{Construction des sédénions $(\Se)$}{Construction of the sedenions $(\Se)$} -Source: \citeannexes{wikipedia_sedenion} +Source : \citeannexes{wikipedia_sedenion} \langsubsection{Table de Cayley}{Cayley's table} %TODO Complete subsection @@ -381,70 +428,55 @@ Source: \citeannexes{wikipedia_sedenion} \hline \end{tabular} - \langsection{Nombres premiers}{Prime numbers} -%TODO Complete section \begin{definition_sq} \label{definition:prime_number} -Un nombre $n \in \N^*$ est dit premier si, et seulement si, ces facteurs sont 1 et lui-même. Sinon ce nombre est dit composé. + \lang{Un nombre $n \in \N \land n \ge 2$ est dit \textbf{premier} si, et seulement si, ces facteurs sont 1 et lui-même. Sinon ce nombre est dit \textbf{composé}.}% + {A number $n \in \N \land n \ge 2$ is \textbf{prime} if, and only if, its factors are 1 and itself. Otherwise this number is \textbf{composé}.} \end{definition_sq} -Par convention, le nombre 1 n'est pas un nombre premier mais cela na pas toujours été le cas. - -\langsubsection{Infinité}{Infinity} +Par convention, le nombre 1 n'est pas un nombre premier, mais cela n'a pas toujours été le cas. \begin{theorem_sq} \label{theorem:prime_infinity} -Il existe une infinité de nombres premiers. + Il existe une infinité de nombres premiers. \end{theorem_sq} \begin{proof} + \lang{Par preuve par contradiction, supposons que le set de nombre premier est fini.}% + {By proof by contraction, let suppose that the set of prime numbers is finite.} -\lang{Par preuve par contradiction, supposons que le set de nombre premier est fini.}% -{By proof by contraction, let suppose that the set of prime numbers is finite.} - -Let $\Pn := \{p \suchthat p \in \N^* \land p \text{\lang{ est premier}{ is prime}}\}$ and $\omega := (\prod\limits_{p\in \Pn} p) + 1$ - -$\implies \forall p \in \Pn$, $\lnot(p \divides \omega)$ - -$\implies (\omega \notin \Pn \land \omega \in \Pn) \implies \bot$ - -$\implies \card{P} = \infty$ + \lang{Soit}{Let} $\Pn := \{p \suchthat p \in \N^*, p$ \lang{ est premier}{ is prime} $\}$ \lang{et}{and} $\omega := (\prod\limits_{p\in \Pn} p) + 1$ + $\implies \forall p \in \Pn, \omega = 1 \mod p \implies \forall p \in \Pn, \lnot(p \divides \omega) \implies \omega$ \lang{est premier}{is prime} $\implies \omega \notin \Pn \land \omega \in \Pn \implies \bot \implies \card{P} = \infty$ \end{proof} -\langsubsection{Irrationalité}{Irrationality} - -\langsubsubsection{$\forall n \in \N, \sqrt{n}$ est soit un nombre premier ou un carré parfait}{$\sqrt{n}$ is either a prime number or a perfect square} - -\begin{theorem_sq} \label{theorem:sqrt_prime} -$\Pn$ is the set of all prime numbers \ref{definition:prime_number}. -$\forall p \in \Pn, \sqrt{p} \notin \Q$ +\begin{theorem_sq} \label{theorem:sqrt_prime_is_irrational} + \lang{La racine carrée d'un nombre premier est irrationnel.}% + {The square root of a prime number is irrational.} \end{theorem_sq} -The classical proof of the irrationality of 2 is a specific case of \ref{theorem:sqrt_prime}. +The classical proof of the irrationality of 2 is a specific case of \ref{theorem:sqrt_prime_is_irrational}. \begin{proof} By contradiction let's assume $\sqrt{p} \in \Q$ -$a \in \Z, b \in \N^*, \gcd(a,b) = 1, \sqrt{p} = \frac{a}{b}$ +$a \in \Z, b \in \N^*, \gcd(a, b) = 1, \sqrt{p} = \frac{a}{b}$ -$\implies p = (\frac{a}{b})^2 = \frac{a^2}{b^2}$ +$\implies p = \left(\frac{a}{b}\right)^2 = \frac{a^2}{b^2} \implies b^2p = a^2 \implies p \divides a$ -$\implies b^2p = a^2$ +Let $c \in \N^*, a = pc$ -$\implies p \divides a$ - -Let $c \in \N^*$, $a = pc$ - -$\implies b^2 p = (pc)^2=p^2c^2$ - -$\implies b^2 = pc^2$ - -$\implies p \divides b$ - -$\implies (p \divides b \land p \divides a \land \gcd(a,b)=1) \implies \bot$ - -$\implies \sqrt{p} \notin \Q$ +$\implies b^2 p = (pc)^2=p^2c^2 \implies b^2 = pc^2 \implies p \divides b \implies (p \divides b \land p \divides a \land \gcd(a, b) = 1) \implies \bot \implies \sqrt{p} \notin \Q$ \end{proof} + +\begin{theorem_sq} + \lang{La racine carrée d'un nombre naturel est soit un nombre premier ou un carré parfait.}% + {The square root of a natural number is either a prime number or a perfect square.} +\end{theorem_sq} + +\begin{proof} + \lipsum[2] + % TODO Complete proof +\end{proof} diff --git a/contents/topology.tex b/contents/topology.tex index b3cde9d..f4d867c 100644 --- a/contents/topology.tex +++ b/contents/topology.tex @@ -129,6 +129,7 @@ Source : \citeannexes{scholarpedia_topological_transitivity} \end{prop_sq} \begin{proof} + \lipsum[2] % TODO Complete proof \end{proof} diff --git a/packages/lstlean.tex b/packages/lstlean.tex new file mode 100644 index 0000000..f92d5ca --- /dev/null +++ b/packages/lstlean.tex @@ -0,0 +1,289 @@ +% Listing style definition for the Lean Theorem Prover. +% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style. +% Unicode replacements taken from Olivier Verdier's unixode.sty + +\lstdefinelanguage{lean} { + +% Anything between $ becomes LaTeX math mode +mathescape=false, +% Comments may or not include Latex commands +texcl=false, + +% keywords, list taken from lean-syntax.el +morekeywords=[1]{ +import, prelude, protected, private, noncomputable, definition, meta, renaming, +hiding, parameter, parameters, begin, constant, constants, +lemma, variable, variables, theory, +print, theorem, example, +open, as, export, override, axiom, axioms, inductive, with, +structure, record, universe, universes, +alias, help, precedence, reserve, declare_trace, add_key_equivalence, +match, infix, infixl, infixr, notation, postfix, prefix, instance, +eval, reduce, check, end, this, +using, using_well_founded, namespace, section, +attribute, local, set_option, extends, include, omit, class, +raw, replacing, +calc, have, show, suffices, by, in, at, let, forall, Pi, fun, +exists, if, dif, then, else, assume, obtain, from, register_simp_ext, unless, break, continue, +mutual, do, def, run_cmd, const, +partial, mut, where, macro, syntax, deriving, +return, try, catch, for, macro_rules, declare_syntax_cat, abbrev}, + +% Sorts +morekeywords=[2]{Sort, Type, Prop}, + +% tactics, list taken from lean-syntax.el +morekeywords=[3]{ +assumption, +apply, intro, intros, allGoals, +generalize, clear, revert, done, exact, +refine, repeat, cases, rewrite, rw, +simp, simp_all, contradiction, +constructor, injection, +induction, group, right, left, use +}, + +% modifiers, taken from lean-syntax.el +% note: 'otherkeywords' is needed because these use a different symbol. +% this command doesn't allow us to specify a number -- they are put with [1] +% otherkeywords={ +% [persistent], [notation], [visible], [instance], [trans_instance], +% [class], [parsing-only], [coercion], [unfold_full], [constructor], +% [reducible], [irreducible], [semireducible], [quasireducible], [wf], +% [whnf], [multiple_instances], [none], [decl], [declaration], +% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify], +% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation], +% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder], +% [localrefinfo], [recursor] +% }, + +% Various symbols +literate= +{α}{{\ensuremath{\mathrm{\alpha}}}}1 +{β}{{\ensuremath{\mathrm{\beta}}}}1 +{γ}{{\ensuremath{\mathrm{\gamma}}}}1 +{δ}{{\ensuremath{\mathrm{\delta}}}}1 +{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1 +{ζ}{{\ensuremath{\mathrm{\zeta}}}}1 +{η}{{\ensuremath{\mathrm{\eta}}}}1 +{θ}{{\ensuremath{\mathrm{\theta}}}}1 +{ι}{{\ensuremath{\mathrm{\iota}}}}1 +{κ}{{\ensuremath{\mathrm{\kappa}}}}1 +{μ}{{\ensuremath{\mathrm{\mu}}}}1 +{ν}{{\ensuremath{\mathrm{\nu}}}}1 +{ξ}{{\ensuremath{\mathrm{\xi}}}}1 +{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1 +{ρ}{{\ensuremath{\mathrm{\rho}}}}1 +{σ}{{\ensuremath{\mathrm{\sigma}}}}1 +{τ}{{\ensuremath{\mathrm{\tau}}}}1 +{φ}{{\ensuremath{\mathrm{\varphi}}}}1 +{χ}{{\ensuremath{\mathrm{\chi}}}}1 +{ψ}{{\ensuremath{\mathrm{\psi}}}}1 +{ω}{{\ensuremath{\mathrm{\omega}}}}1 + +{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1 +{Δ}{{\ensuremath{\mathrm{\Delta}}}}1 +{Θ}{{\ensuremath{\mathrm{\Theta}}}}1 +{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1 +{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Φ}{{\ensuremath{\mathrm{\Phi}}}}1 +{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1 +{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1 +{Ω}{{\ensuremath{\mathrm{\Omega}}}}1 + +{ℵ}{{\ensuremath{\aleph}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 +{≠}{{\ensuremath{\neq}}}1 +{≈}{{\ensuremath{\approx}}}1 +{≡}{{\ensuremath{\equiv}}}1 +{≃}{{\ensuremath{\simeq}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 + +{∂}{{\ensuremath{\partial}}}1 +{∆}{{\ensuremath{\triangle}}}1 % or \laplace? + +{∫}{{\ensuremath{\int}}}1 +{∑}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Π}{{\ensuremath{\mathrm{\Pi}}}}1 + +{⊥}{{\ensuremath{\perp}}}1 +{∞}{{\ensuremath{\infty}}}1 +{∂}{{\ensuremath{\partial}}}1 + +{∓}{{\ensuremath{\mp}}}1 +{±}{{\ensuremath{\pm}}}1 +{×}{{\ensuremath{\times}}}1 + +{⊕}{{\ensuremath{\oplus}}}1 +{⊗}{{\ensuremath{\otimes}}}1 +{⊞}{{\ensuremath{\boxplus}}}1 + +{∇}{{\ensuremath{\nabla}}}1 +{√}{{\ensuremath{\sqrt}}}1 + +{⬝}{{\ensuremath{\cdot}}}1 +{•}{{\ensuremath{\cdot}}}1 +{∘}{{\ensuremath{\circ}}}1 + +%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1 +{⁻}{{\ensuremath{^{-}}}}1 +{▸}{{\ensuremath{\blacktriangleright}}}1 + +{∧}{{\ensuremath{\wedge}}}1 +{∨}{{\ensuremath{\vee}}}1 +{¬}{{\ensuremath{\neg}}}1 +{⊢}{{\ensuremath{\vdash}}}1 + +%{⟨}{{\ensuremath{\left\langle}}}1 +%{⟩}{{\ensuremath{\right\rangle}}}1 +{⟨}{{\ensuremath{\langle}}}1 +{⟩}{{\ensuremath{\rangle}}}1 + +{↦}{{\ensuremath{\mapsto}}}1 +{←}{{\ensuremath{\leftarrow}}}1 +{<-}{{\ensuremath{\leftarrow}}}1 +{→}{{\ensuremath{\rightarrow}}}1 +{↔}{{\ensuremath{\leftrightarrow}}}1 +{⇒}{{\ensuremath{\Rightarrow}}}1 +{⟹}{{\ensuremath{\Longrightarrow}}}1 +{⇐}{{\ensuremath{\Leftarrow}}}1 +{⟸}{{\ensuremath{\Longleftarrow}}}1 + +{∩}{{\ensuremath{\cap}}}1 +{∪}{{\ensuremath{\cup}}}1 +{⊂}{{\ensuremath{\subseteq}}}1 +{⊆}{{\ensuremath{\subseteq}}}1 +{⊄}{{\ensuremath{\nsubseteq}}}1 +{⊈}{{\ensuremath{\nsubseteq}}}1 +{⊃}{{\ensuremath{\supseteq}}}1 +{⊇}{{\ensuremath{\supseteq}}}1 +{⊅}{{\ensuremath{\nsupseteq}}}1 +{⊉}{{\ensuremath{\nsupseteq}}}1 +{∈}{{\ensuremath{\in}}}1 +{∉}{{\ensuremath{\notin}}}1 +{∋}{{\ensuremath{\ni}}}1 +{∌}{{\ensuremath{\notni}}}1 +{∅}{{\ensuremath{\emptyset}}}1 + +{∖}{{\ensuremath{\setminus}}}1 +{†}{{\ensuremath{\dag}}}1 + +{ℕ}{{\ensuremath{\mathbb{N}}}}1 +{ℤ}{{\ensuremath{\mathbb{Z}}}}1 +{ℝ}{{\ensuremath{\mathbb{R}}}}1 +{ℚ}{{\ensuremath{\mathbb{Q}}}}1 +{ℂ}{{\ensuremath{\mathbb{C}}}}1 +{⌞}{{\ensuremath{\llcorner}}}1 +{⌟}{{\ensuremath{\lrcorner}}}1 +{⦃}{{\ensuremath{\{\!|}}}1 +{⦄}{{\ensuremath{|\!\}}}}1 + +{‖}{{\ensuremath{\|}}}1 +{₁}{{\ensuremath{_1}}}1 +{₂}{{\ensuremath{_2}}}1 +{₃}{{\ensuremath{_3}}}1 +{₄}{{\ensuremath{_4}}}1 +{₅}{{\ensuremath{_5}}}1 +{₆}{{\ensuremath{_6}}}1 +{₇}{{\ensuremath{_7}}}1 +{₈}{{\ensuremath{_8}}}1 +{₉}{{\ensuremath{_9}}}1 +{₀}{{\ensuremath{_0}}}1 +{ᵢ}{{\ensuremath{_i}}}1 +{ⱼ}{{\ensuremath{_j}}}1 +{ₐ}{{\ensuremath{_a}}}1 + +{¹}{{\ensuremath{^1}}}1 + +{ₙ}{{\ensuremath{_n}}}1 +{ₘ}{{\ensuremath{_m}}}1 +{ₚ}{{\ensuremath{_p}}}1 +{↑}{{\ensuremath{\uparrow}}}1 +{↓}{{\ensuremath{\downarrow}}}1 + +{...}{{\ensuremath{\ldots}}}1 +{·}{{\ensuremath{\cdot}}}1 + +{▸}{{\ensuremath{\triangleright}}}1 + +{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1 +{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1 +{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1 +{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1 +{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1 +{\$}{{\color{symbolcolor}\$}}1 + +{:=}{{\color{symbolcolor}:=}}1 +{=}{{\color{symbolcolor}=}}1 +{<|>}{{\color{symbolcolor}<|>}}1 +{<\$>}{{\color{symbolcolor}<\$>}}1 +{+}{{\color{symbolcolor}+}}1 +{*}{{\color{symbolcolor}*}}1, + +% Comments +%comment=[s][\itshape \color{commentcolor}]{/-}{-/}, +morecomment=[s][\color{commentcolor}]{/-}{-/}, +morecomment=[l][\itshape \color{commentcolor}]{--}, + +% Spaces are not displayed as a special character +showstringspaces=false, + +% keep spaces +keepspaces=true, + +% String delimiters +morestring=[b]", +morestring=[d]’, + +% Size of tabulations +tabsize=3, + +% Enables ASCII chars 128 to 255 +extendedchars=false, + +% Case sensitivity +sensitive=true, + +% Automatic breaking of long lines +breaklines=true, +breakatwhitespace=true, + +% Default style fors listingsred +basicstyle=\ttfamily\small, + +% Position of captions is bottom +captionpos=b, + +% Full flexible columns +columns=[l]fullflexible, + + +% Style for (listings') identifiers +identifierstyle={\ttfamily\color{identifiercolor}}, +% Note : highlighting of Coq identifiers is done through a new +% delimiter definition through an lstset at the beginning of the +% document. Don't know how to do better. + +% Style for declaration keywords +keywordstyle=[1]{\ttfamily\color{keywordcolor}}, + +% Style for sorts +keywordstyle=[2]{\ttfamily\color{sortcolor}}, + +% Style for tactics keywords +keywordstyle=[3]{\ttfamily\color{tacticcolor}}, + +% Style for attributes +keywordstyle=[4]{\ttfamily\color{attributecolor}}, + +% Style for strings +stringstyle={\ttfamily\color{white}}, + +% Style for comments +commentstyle={\ttfamily\footnotesize }, + +} diff --git a/packages/macros.sty b/packages/macros.sty index c16f3c0..4f2f7ba 100644 --- a/packages/macros.sty +++ b/packages/macros.sty @@ -20,6 +20,7 @@ \newcommand{\Cat}{\mathcal{C}} % Category \newcommand{\Set}{\mathbf{Set}} % Set category \newcommand{\Grp}{\mathbf{Grp}} % Group category +\newcommand{\Ring}{\mathbf{Ring}} % Ring category \newcommand{\Ab}{\mathbf{Ab}} % Abelian category \newcommand{\Top}{\mathbf{Top}} % Topological spaces category \newcommand{\K}{\mathbb{K}} % Corps @@ -43,15 +44,18 @@ \newtheorem{definition}{\lang{Définition}{Definition}} \newtheorem{theorem}{\lang{Théorème}{Theoreme}} \newtheorem{lemme}{Lemme} +\newtheorem{exercise}{\lang{Exercice}{Exercise}} \newcommandx{\suite}[3][1=n,2=n]{$(#3_{#1})_{#2 \in \N}$} \newcommand{\innerproduct}[2]{\langle #1, #2 \rangle} -\newenvironment{definition_sq}{\begin{mdframed}\begin{definition}}{\end{definition}\end{mdframed}} -\newenvironment{theorem_sq}{\begin{mdframed}\begin{theorem}}{\end{theorem}\end{mdframed}} -\newenvironment{lemme_sq}{\begin{mdframed}\begin{lemme}}{\end{lemme}\end{mdframed}} +\newenvironment{definition_sq}[1][]{\begin{mdframed}\begin{definition}[#1]}{\end{definition}\end{mdframed}} +\newenvironment{theorem_sq}[1][]{\begin{mdframed}\begin{theorem}[#1]}{\end{theorem}\end{mdframed}} +\newenvironment{lemme_sq}[1][]{\begin{mdframed}\begin{lemme}[#1]}{\end{lemme}\end{mdframed}} \newtheorem{prop}{Proposition} -\newenvironment{prop_sq}{\begin{mdframed}\begin{prop}}{\end{prop}\end{mdframed}} +\newenvironment{prop_sq}[1][]{\begin{mdframed}\begin{prop}[#1]}{\end{prop}\end{mdframed}} \newtheorem{corollary}{Corollaire} -\newenvironment{corollary_sq}{\begin{mdframed}\begin{corollary}}{\end{corollary}\end{mdframed}} +\newenvironment{corollary_sq}[1][]{\begin{mdframed}\begin{corollary}[#1]}{\end{corollary}\end{mdframed}} +\newenvironment{exercise_sq}[1][]{\begin{mdframed}\begin{exercise}[#1]}{\end{exercise}\end{mdframed}} +\newcommand{\inv}[1]{#1^{-1}} \DeclarePairedDelimiter{\generator}{\langle}{\rangle} \DeclareMathOperator{\subgroup}{\leqslant} \DeclareMathOperator{\normalSubgroup}{\trianglelefteq} @@ -74,6 +78,7 @@ \newcommand{\functiondef}[2]{\hspace{15pt}#1 \longmapsto #2} \newcommand{\otherwise}{\text{\lang{Sinon}{Otherwise}}} \DeclareMathOperator{\union}{\cup} +\DeclareMathOperator{\distinctUnion}{\sqcup} \DeclareMathOperator{\Union}{\bigcup} \DeclareMathOperator{\intersection}{\cap} \DeclareMathOperator{\Intersection}{\bigcap} diff --git a/packages/themes.sty b/packages/themes.sty index 77fdc0f..d1675f7 100644 --- a/packages/themes.sty +++ b/packages/themes.sty @@ -2,11 +2,12 @@ % Add many functions for colour themes \RequirePackage{xcolor} +% Code highlighting +\RequirePackage{listings} \DeclareOption{default}{\OptionNotUsed} \definecolor{theme_colour_background} {RGB} {255, 255, 255} \definecolor{theme_colour_foreground} {RGB} {0, 0, 0 } -\definecolor{theme_colour_cl} {RGB} {68, 71, 90 } \definecolor{theme_colour_comment} {RGB} {98, 114, 164} \definecolor{theme_colour_cyan} {RGB} {139, 233, 253} \definecolor{theme_colour_green} {RGB} {0, 255, 0 } @@ -16,10 +17,17 @@ \definecolor{theme_colour_red} {RGB} {255, 0, 0 } \definecolor{theme_colour_yellow} {RGB} {255, 255, 0 } +\definecolor{identifiercolor} {named} {theme_colour_foreground} +\definecolor{keywordcolor} {named} {theme_colour_purple} +\definecolor{tacticcolor} {named} {theme_colour_purple} +\definecolor{symbolcolor} {named} {theme_colour_foreground} +\definecolor{sortcolor} {named} {theme_colour_green} +\definecolor{attributecolor} {named} {theme_colour_cyan} +\definecolor{commentcolor} {named} {theme_colour_comment} + \DeclareOption{codedark}{ \definecolor{theme_colour_background} {HTML} {222324} \definecolor{theme_colour_foreground} {HTML} {FFFFFF} - \definecolor{theme_colour_cl} {RGB} {68, 71, 90 } \definecolor{theme_colour_comment} {RGB} {98, 114, 164} \definecolor{theme_colour_cyan} {RGB} {139, 233, 253} \definecolor{theme_colour_green} {RGB} {80, 250, 123} @@ -28,12 +36,19 @@ \definecolor{theme_colour_purple} {RGB} {189, 147, 249} \definecolor{theme_colour_red} {RGB} {255, 85, 85 } \definecolor{theme_colour_yellow} {RGB} {241, 250, 140} + + \definecolor{identifiercolor} {named} {theme_colour_foreground} + \definecolor{keywordcolor} {named} {theme_colour_purple} + \definecolor{tacticcolor} {named} {theme_colour_purple} + \definecolor{symbolcolor} {named} {theme_colour_foreground} + \definecolor{sortcolor} {named} {theme_colour_green} + \definecolor{attributecolor} {named} {theme_colour_cyan} + \definecolor{commentcolor} {named} {theme_colour_comment} } \DeclareOption{dracula}{ \definecolor{theme_colour_background} {RGB} {40, 42, 54 } \definecolor{theme_colour_foreground} {RGB} {248, 248, 242} - \definecolor{theme_colour_cl} {RGB} {68, 71, 90 } \definecolor{theme_colour_comment} {RGB} {98, 114, 164} \definecolor{theme_colour_cyan} {RGB} {139, 233, 253} \definecolor{theme_colour_green} {RGB} {80, 250, 123} @@ -42,6 +57,16 @@ \definecolor{theme_colour_purple} {RGB} {189, 147, 249} \definecolor{theme_colour_red} {RGB} {255, 85, 85 } \definecolor{theme_colour_yellow} {RGB} {241, 250, 140} + + \definecolor{identifiercolor} {named} {theme_colour_foreground} + \definecolor{keywordcolor} {named} {theme_colour_purple} + \definecolor{tacticcolor} {named} {theme_colour_purple} + \definecolor{symbolcolor} {named} {theme_colour_foreground} + \definecolor{sortcolor} {named} {theme_colour_green} + \definecolor{attributecolor} {named} {theme_colour_cyan} + \definecolor{commentcolor} {named} {theme_colour_comment} } +\edef\lstlanguagefiles{\lstlanguagefiles,packages/lstlean.tex} + \ProcessOptions\relax