link fix

blueprint/src/demo.tex

@@ -68,7 +68,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:disc_of_prim_elt_basis}
-	\lean{algebra.discr_power_basis_eq_prod}
+	\lean{Algebra.discr_powerBasis_eq_prod}
 	\leanok
 	\uses{defn_of_disc,lemma:disc_via_embs}
 	Let $K$ be a number field and $B=\{1,\a,\a^2,\dots,\a^{n-1}\}$ for some $\a \in K$. Then \[\Delta(B)=\prod_{i < j} (\sigma_i(\a)-\sigma_j(\a))^2\] where $\sigma_i$ are the embeddings of $K $ into $\CC$. Here $\Delta(B)$ denotes the discriminant.
@@ -80,7 +80,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:diff_of_irr_pol}
-	\lean{polynomial.aeval_root_derivative_of_splits}
+	\lean{Polynomial.aeval_root_derivative_of_splits}
 	\leanok
 	Let $f$ be a monic irreducible polynomial over a number field $K$ and let $\a$ be one of its roots in $\CC$. Then \[f'(\a)=\prod_{\beta \neq \a} (\a-\beta),  \] where the product is over the roots of $f$ different from $\a$.
 \end{lemma}
@@ -90,7 +90,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:num_field_disc_in_terms_of_norm}
-	\lean{algebra.discr_power_basis_eq_norm}
+	\lean{Algebra.discr_powerBasis_eq_norm}
 	\leanok
 	\uses{lemma:disc_of_prim_elt_basis,lemma:alt_definition_of_norm, lemma:diff_of_irr_pol}
 	Let $K=\QQ(\a)$ be a number field with $n=[K:\QQ]$ and let $B=\{1,\a,\a^2,\dots,\a^{n-1}\}$. Then \[\Delta(B)=(-1)^{\frac{n(n-1)}{2}}N_{K/\QQ}(m_\a'(\a))\] where $m_\a'$ is the derivative of $m_\a(x)$ (which we recall denotes the minimal polynomial of $\a$).
@@ -103,7 +103,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:norm_of_alg_int_is_int}
-	\lean{algebra.is_integral_norm}
+	\lean{Algebra.isIntegral_norm}
 	\leanok
 	If $K$ is a number field and $\a \in \OO_K$ then $N_{K/\QQ}(\a)$ is in $\ZZ$.
 \end{lemma}
@@ -113,7 +113,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:trace_of_alg_int_is_int}
-	\lean{algebra.is_integral_trace}
+	\lean{Algebra.isIntegral_trace}
 	\leanok
 	If $K$ is a number field and $\a \in \OO_K$ then $\Tr_{K/\QQ}(\a)$ is in $\ZZ$.
 \end{lemma}
@@ -123,7 +123,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:int_basis_int_disc}
-	\lean{algebra.discr_is_integral}
+	\lean{Algebra.discr_isIntegral}
 	\leanok
 	\uses{defn_of_disc,lemma:trace_of_alg_int_is_int}
 	Let $K$ be a number field and $B=\{b_1,\dots,b_n\}$ be elements in $\OO_K$, then $\Delta(B) \in \ZZ$.
@@ -135,7 +135,7 @@ \section{Discriminants of number fields}
 
 
 \begin{lemma}\label{lemma:disc_int_basis}
-	\lean{algebra.discr_mul_is_integral_mem_adjoin}
+	\lean{Algebra.discr_mul_isIntegral_mem_adjoin}
 	\leanok
 	\uses{lem:disc_change_of_basis,lemma:int_basis_int_disc}
 	Let $K = \QQ(\alpha)$ be a number field, where $\alpha$ is an algebraic integer. Let $B = \{1, \alpha, \ldots, \alpha^{[K : \QQ] - 1} \}$ be the basis given by $\alpha$ and let $x \in \mathcal{O}_K$. Then $\Delta(B)x \in \ZZ[\alpha]$.
@@ -147,7 +147,7 @@ \section{Discriminants of number fields}
 \end{proof}
 
 \begin{lemma}\label{lemma:eis_crit_and_alg_ints}
-	\lean{mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at}
+	\lean{mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt}
 	\leanok
 	\uses{lemma:norm_of_alg_int_is_int,lemma:trace_of_alg_int_is_int}
 	Let $K = \QQ(\alpha)$ be a number field, where $\alpha$ is an algebraic integer with minimal polynomial that is Eisenstein at $p$. Let $x \in \mathcal{O}_K$ such that $p^n x \in \ZZ[\alpha]$ for some $n$. Then $x \in \ZZ[\alpha]$.
@@ -160,7 +160,7 @@ \section{Discriminants of number fields}
 \section{Cyclotomic fields}
 
 \begin{lemma}\label{lemma:cyclo_poly_deg}
-	\lean{polynomial.degree_cyclotomic}
+	\lean{Polynomial.degree_cyclotomic}
 	\leanok
 	For $n$ any integer, $\Phi_n$ (the $n$-th cyclotomic polynomial) is a polynomial of degree $\varphi(n)$ (where $\varphi$ is Euler's Totient function).
 \end{lemma}
@@ -171,7 +171,7 @@ \section{Cyclotomic fields}
 
 
 \begin{lemma}\label{lemma:cyclo_poly_irr}
-	\lean{polynomial.cyclotomic.irreducible}
+	\lean{Polynomial.cyclotomic.irreducible}
 	\leanok
 	For $n$ any integer, $\Phi_n$ (the $n$-th cyclotomic polynomial) is an irreducible polynomial .
 \end{lemma}
@@ -183,7 +183,7 @@ \section{Cyclotomic fields}
 \begin{lemma}\label{lem:discr_of_cyclo}
 	\uses{lemma:num_field_disc_in_terms_of_norm,lemma:cyclo_poly_irr,lemma:cyclo_poly_deg}
 	\leanok
-	\lean{is_cyclotomic_extension.rat.discr_prime_pow'}
+	\lean{IsCyclotomicExtension.Rat.discr_prime_pow'}
 	Let $\zeta_p$ be a $p$-th root of unity for $p$ an odd prime, let $\lam_p=1-\zeta_p$ and $K=\QQ(\zeta_p)$. Then \[\Delta(\{1,\zeta_p,\dots,\zeta_p^{p-2}\})=\Delta(\{1,\lam_p,\dots,\lam_p^{p-2}\})=(-1)^{\frac{(p-1)}{2}}p^{p-2}.\]
 \end{lemma}
 \begin{proof}
@@ -201,7 +201,7 @@ \section{Cyclotomic fields}
 \begin{theorem}\label{theorem:ring_of_ints_of_cyclo}
 	\uses{lem:discr_of_cyclo,lemma:eis_crit_and_alg_ints,lemma:disc_int_basis}
 	\leanok
-	\lean{is_cyclotomic_extension.rat.is_integral_closure_adjoing_singleton_of_prime}
+	\lean{IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow}
 	Let $\zeta_p$ be a $p$-th root of unity for $p$ an odd prime, let $\lam_p=1-\zeta_p$ and $K=\QQ(\zeta_p)$. Then $\OO_K=\ZZ[\zeta_p]=\ZZ[\lam_p]$.
 \end{theorem}
 \begin{proof}
@@ -310,7 +310,7 @@ \section{Fermat's Last Theorem for regular primes}
 \end{proof}
 
 \begin{lemma}\label{lemma:may_assume_coprime}
-	\lean{flt_regular.caseI.may_assume}
+	\lean{FltRegular.CaseI.may_assume}
 	\leanok
 	\uses{lemma:unit_lemma,lemma:zeta_pow_sub_eq_unit_zeta_sub_one,lemma:ideals_mult_to_power,theorem:ring_of_ints_of_cyclo}
 
@@ -331,13 +331,13 @@ \section{Fermat's Last Theorem for regular primes}
 \end{proof}
 
 \begin{definition}\label{defn:is_regular_number}
-	\lean{is_regular_number}
+	\lean{IsRegularNumber}
 	\leanok
 	A prime number $p$ is called regular if it does not divide the class number of $\QQ(\zeta_p)$.
 \end{definition}
 
 \begin{theorem}\label{theorem:FLT_case_one}
-	\lean{flt_regular.caseI}
+	\lean{FltRegular.caseI}
 	\leanok
 	\uses{defn:is_regular_number,lem:exists_int_sum_eq_zero,lem:dvd_coeff_cycl_integer,lemma:may_assume_coprime,lem:flt_ideals_coprime}
 	Let $p$ be an odd regular prime. Then \[x^p+y^p=z^p\] has no solutions with $x,y,z \in \ZZ$ and $\gcd(xyz,p)=1$.
@@ -385,7 +385,7 @@ \section{Fermat's Last Theorem for regular primes}
 \end{theorem}
 
 \begin{theorem}\label{theorem:FLT_case_two}
-	\lean{flt_regular.caseII}
+	\lean{FltRegular.caseII}
 	\leanok
 	\uses{lemma:defn:is_regular_number,thm:Kummers_lemma, thm:gen_flt_eqn}
 	Let $p$ be an odd regular prime. Then \[x^p+y^p=z^p\] has no solutions with $x,y,z \in \ZZ$ and $p | xyz$.