Skip to content

Commit

Permalink
test6
Browse files Browse the repository at this point in the history
  • Loading branch information
@CBirkbeck
CBirkbeck committed Oct 4, 2023
1 parent aafc51a commit 77ec1bc
Show file tree
Hide file tree
Showing 7 changed files with 60 additions and 62 deletions.
82 changes: 40 additions & 42 deletions blueprint/print/print.aux
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,47 +22,45 @@
\citation{washington}
\HyPL@Entry{0<</S/D>>}
\babel@aux{english}{}
\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Demo}}{1}{section.1}\protected@file@percent }
\newlabel{cha:demo}{{1}{1}{Demo}{section.1}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{Introduction}}{1}{section.2}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Discriminants of number fields}}{1}{section.3}\protected@file@percent }
\newlabel{lemma:alt_definition_of_norm}{{3.1}{1}{}{subsection.3.1}{}}
\newlabel{lemma:alt_definition_of_trace}{{3.2}{1}{}{subsection.3.2}{}}
\newlabel{defn_of_disc}{{3.3}{1}{}{subsection.3.3}{}}
\newlabel{lem:lin_indep_iff_disc_ne_zero}{{3.4}{2}{}{subsection.3.4}{}}
\newlabel{lem:disc_change_of_basis}{{3.5}{2}{}{subsection.3.5}{}}
\newlabel{lemma:disc_via_embs}{{3.6}{2}{}{subsection.3.6}{}}
\newlabel{lemma:disc_of_prim_elt_basis}{{3.7}{2}{}{subsection.3.7}{}}
\newlabel{lemma:diff_of_irr_pol}{{3.8}{2}{}{subsection.3.8}{}}
\newlabel{lemma:num_field_disc_in_terms_of_norm}{{3.9}{3}{}{subsection.3.9}{}}
\newlabel{lemma:norm_of_alg_int_is_int}{{3.10}{3}{}{subsection.3.10}{}}
\newlabel{lemma:trace_of_alg_int_is_int}{{3.11}{3}{}{subsection.3.11}{}}
\newlabel{lemma:int_basis_int_disc}{{3.12}{3}{}{subsection.3.12}{}}
\newlabel{lemma:disc_int_basis}{{3.13}{3}{}{subsection.3.13}{}}
\newlabel{lemma:eis_crit_and_alg_ints}{{3.14}{3}{}{subsection.3.14}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{Cyclotomic fields}}{4}{section.4}\protected@file@percent }
\newlabel{lemma:cyclo_poly_deg}{{4.1}{4}{}{subsection.4.1}{}}
\newlabel{lemma:cyclo_poly_irr}{{4.2}{4}{}{subsection.4.2}{}}
\newlabel{lem:discr_of_cyclo}{{4.3}{4}{}{subsection.4.3}{}}
\newlabel{theorem:ring_of_ints_of_cyclo}{{4.4}{4}{}{subsection.4.4}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Introduction}}{1}{section.1}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{Discriminants of number fields}}{1}{section.2}\protected@file@percent }
\newlabel{lemma:alt_definition_of_norm}{{2.1}{1}{}{subsection.2.1}{}}
\newlabel{lemma:alt_definition_of_trace}{{2.2}{1}{}{subsection.2.2}{}}
\newlabel{defn_of_disc}{{2.3}{1}{}{subsection.2.3}{}}
\newlabel{lem:lin_indep_iff_disc_ne_zero}{{2.4}{2}{}{subsection.2.4}{}}
\newlabel{lem:disc_change_of_basis}{{2.5}{2}{}{subsection.2.5}{}}
\newlabel{lemma:disc_via_embs}{{2.6}{2}{}{subsection.2.6}{}}
\newlabel{lemma:disc_of_prim_elt_basis}{{2.7}{2}{}{subsection.2.7}{}}
\newlabel{lemma:diff_of_irr_pol}{{2.8}{2}{}{subsection.2.8}{}}
\newlabel{lemma:num_field_disc_in_terms_of_norm}{{2.9}{3}{}{subsection.2.9}{}}
\newlabel{lemma:norm_of_alg_int_is_int}{{2.10}{3}{}{subsection.2.10}{}}
\newlabel{lemma:trace_of_alg_int_is_int}{{2.11}{3}{}{subsection.2.11}{}}
\newlabel{lemma:int_basis_int_disc}{{2.12}{3}{}{subsection.2.12}{}}
\newlabel{lemma:disc_int_basis}{{2.13}{3}{}{subsection.2.13}{}}
\newlabel{lemma:eis_crit_and_alg_ints}{{2.14}{3}{}{subsection.2.14}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Cyclotomic fields}}{4}{section.3}\protected@file@percent }
\newlabel{lemma:cyclo_poly_deg}{{3.1}{4}{}{subsection.3.1}{}}
\newlabel{lemma:cyclo_poly_irr}{{3.2}{4}{}{subsection.3.2}{}}
\newlabel{lem:discr_of_cyclo}{{3.3}{4}{}{subsection.3.3}{}}
\newlabel{theorem:ring_of_ints_of_cyclo}{{3.4}{4}{}{subsection.3.4}{}}
\citation{washington}
\citation{marcus}
\newlabel{lemma:alg_int_abs_val_one}{{4.5}{5}{}{subsection.4.5}{}}
\newlabel{lem:roots_of_unity_in_cyclo}{{4.6}{5}{}{subsection.4.6}{}}
\newlabel{lemma:unit_lemma}{{4.7}{5}{}{subsection.4.7}{}}
\newlabel{lemma:zeta_pow_sub_eq_unit_zeta_sub_one}{{4.8}{5}{}{subsection.4.8}{}}
\newlabel{lemma:ideals_mult_to_power}{{4.9}{5}{}{subsection.4.9}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{5}{Fermat's Last Theorem for regular primes}}{5}{section.5}\protected@file@percent }
\newlabel{lem:flt_ideals_coprime}{{5.1}{5}{}{subsection.5.1}{}}
\newlabel{lem:exists_int_sub_pow_prime_dvd}{{5.2}{6}{}{subsection.5.2}{}}
\newlabel{lem:dvd_coeff_cycl_integer}{{5.3}{6}{}{subsection.5.3}{}}
\newlabel{lem:exists_int_sum_eq_zero}{{5.4}{6}{}{subsection.5.4}{}}
\newlabel{lemma:may_assume_coprime}{{5.5}{6}{}{subsection.5.5}{}}
\newlabel{lemma:alg_int_abs_val_one}{{3.5}{5}{}{subsection.3.5}{}}
\newlabel{lem:roots_of_unity_in_cyclo}{{3.6}{5}{}{subsection.3.6}{}}
\newlabel{lemma:unit_lemma}{{3.7}{5}{}{subsection.3.7}{}}
\newlabel{lemma:zeta_pow_sub_eq_unit_zeta_sub_one}{{3.8}{5}{}{subsection.3.8}{}}
\newlabel{lemma:ideals_mult_to_power}{{3.9}{5}{}{subsection.3.9}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{4}{Fermat's Last Theorem for regular primes}}{5}{section.4}\protected@file@percent }
\newlabel{lem:flt_ideals_coprime}{{4.1}{5}{}{subsection.4.1}{}}
\newlabel{lem:exists_int_sub_pow_prime_dvd}{{4.2}{6}{}{subsection.4.2}{}}
\newlabel{lem:dvd_coeff_cycl_integer}{{4.3}{6}{}{subsection.4.3}{}}
\newlabel{lem:exists_int_sum_eq_zero}{{4.4}{6}{}{subsection.4.4}{}}
\newlabel{lemma:may_assume_coprime}{{4.5}{6}{}{subsection.4.5}{}}
\citation{Borevich_Shafarevich}
\newlabel{defn:is_regular_number}{{5.6}{7}{}{subsection.5.6}{}}
\newlabel{theorem:FLT_case_one}{{5.7}{7}{}{subsection.5.7}{}}
\newlabel{thm:Kummers_lemma}{{5.8}{7}{}{subsection.5.8}{}}
\newlabel{lem:gen_dvd_by_frak_p}{{5.9}{7}{}{subsection.5.9}{}}
\newlabel{defn:is_regular_number}{{4.6}{7}{}{subsection.4.6}{}}
\newlabel{theorem:FLT_case_one}{{4.7}{7}{}{subsection.4.7}{}}
\newlabel{thm:Kummers_lemma}{{4.8}{7}{}{subsection.4.8}{}}
\newlabel{lem:gen_dvd_by_frak_p}{{4.9}{7}{}{subsection.4.9}{}}
\bibstyle{amsalpha}
\bibdata{references}
\bibcite{Borevich_Shafarevich}{BS66}
Expand All @@ -74,9 +72,9 @@
\newlabel{tocindent1}{19.4691pt}
\newlabel{tocindent2}{0pt}
\newlabel{tocindent3}{0pt}
\newlabel{lem:gen_ideal_coprimality}{{5.10}{8}{}{subsection.5.10}{}}
\newlabel{thm:gen_flt_eqn}{{5.11}{8}{}{subsection.5.11}{}}
\newlabel{theorem:FLT_case_two}{{5.12}{8}{}{subsection.5.12}{}}
\newlabel{FLT_regular}{{5.13}{8}{}{subsection.5.13}{}}
\newlabel{lem:gen_ideal_coprimality}{{4.10}{8}{}{subsection.4.10}{}}
\newlabel{thm:gen_flt_eqn}{{4.11}{8}{}{subsection.4.11}{}}
\newlabel{theorem:FLT_case_two}{{4.12}{8}{}{subsection.4.12}{}}
\newlabel{FLT_regular}{{4.13}{8}{}{subsection.4.13}{}}
\@writefile{toc}{\contentsline {section}{\tocsection {}{}{References}}{8}{section*.2}\protected@file@percent }
\gdef \@abspage@last{8}
15 changes: 9 additions & 6 deletions blueprint/print/print.log
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
This is XeTeX, Version 3.141592653-2.6-0.999993 (MiKTeX 21.8) (preloaded format=xelatex 2023.10.4) 4 OCT 2023 12:48
This is XeTeX, Version 3.141592653-2.6-0.999993 (MiKTeX 21.8) (preloaded format=xelatex 2023.10.4) 4 OCT 2023 18:07
entering extended mode
**./print.tex
(print.tex
Expand Down Expand Up @@ -405,14 +405,17 @@ File: ueuf.fd 2013/01/14 v3.01 Euler Fraktur
[5] [6] [7]))
(C:\Users\chris\FLT_regular_blueprint\FltRegular\blueprint\print\print.bbl)
[8] (C:\Users\chris\FLT_regular_blueprint\FltRegular\blueprint\print\print.aux)

LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

Package rerunfilecheck Info: File `print.out' has not changed.
(rerunfilecheck) Checksum: 1D925A8B4B9B9F10A1E92BA71BF0A2F2;941.
(rerunfilecheck) Checksum: A8E1EAC795EDE6729C459F2A0F378DAD;860.
)
Here is how much of TeX's memory you used:
10460 strings out of 411335
149041 string characters out of 2832716
491447 words of memory out of 3000000
30542 multiletter control sequences out of 15000+600000
10459 strings out of 411335
149031 string characters out of 2832716
491318 words of memory out of 3000000
30541 multiletter control sequences out of 15000+600000
411400 words of font info for 66 fonts, out of 8000000 for 9000
1509 hyphenation exceptions out of 8191
71i,8n,80p,1028b,448s stack positions out of 5000i,500n,10000p,200000b,80000s
Expand Down
11 changes: 5 additions & 6 deletions blueprint/print/print.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
\BOOKMARK [1][-]{section.1}{\376\377\0001\000.\000\040\000D\000e\000m\000o}{}% 1
\BOOKMARK [1][-]{section.2}{\376\377\0002\000.\000\040\000I\000n\000t\000r\000o\000d\000u\000c\000t\000i\000o\000n}{}% 2
\BOOKMARK [1][-]{section.3}{\376\377\0003\000.\000\040\000D\000i\000s\000c\000r\000i\000m\000i\000n\000a\000n\000t\000s\000\040\000o\000f\000\040\000n\000u\000m\000b\000e\000r\000\040\000f\000i\000e\000l\000d\000s}{}% 3
\BOOKMARK [1][-]{section.4}{\376\377\0004\000.\000\040\000C\000y\000c\000l\000o\000t\000o\000m\000i\000c\000\040\000f\000i\000e\000l\000d\000s}{}% 4
\BOOKMARK [1][-]{section.5}{\376\377\0005\000.\000\040\000F\000e\000r\000m\000a\000t\000'\000s\000\040\000L\000a\000s\000t\000\040\000T\000h\000e\000o\000r\000e\000m\000\040\000f\000o\000r\000\040\000r\000e\000g\000u\000l\000a\000r\000\040\000p\000r\000i\000m\000e\000s}{}% 5
\BOOKMARK [1][-]{section*.2}{\376\377\000R\000e\000f\000e\000r\000e\000n\000c\000e\000s}{}% 6
\BOOKMARK [1][-]{section.1}{\376\377\0001\000.\000\040\000I\000n\000t\000r\000o\000d\000u\000c\000t\000i\000o\000n}{}% 1
\BOOKMARK [1][-]{section.2}{\376\377\0002\000.\000\040\000D\000i\000s\000c\000r\000i\000m\000i\000n\000a\000n\000t\000s\000\040\000o\000f\000\040\000n\000u\000m\000b\000e\000r\000\040\000f\000i\000e\000l\000d\000s}{}% 2
\BOOKMARK [1][-]{section.3}{\376\377\0003\000.\000\040\000C\000y\000c\000l\000o\000t\000o\000m\000i\000c\000\040\000f\000i\000e\000l\000d\000s}{}% 3
\BOOKMARK [1][-]{section.4}{\376\377\0004\000.\000\040\000F\000e\000r\000m\000a\000t\000'\000s\000\040\000L\000a\000s\000t\000\040\000T\000h\000e\000o\000r\000e\000m\000\040\000f\000o\000r\000\040\000r\000e\000g\000u\000l\000a\000r\000\040\000p\000r\000i\000m\000e\000s}{}% 4
\BOOKMARK [1][-]{section*.2}{\376\377\000R\000e\000f\000e\000r\000e\000n\000c\000e\000s}{}% 5
Binary file modified blueprint/print/print.pdf
View file
Binary file not shown.
9 changes: 4 additions & 5 deletions blueprint/print/print.toc
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
\babel@toc {english}{}\relax
\contentsline {section}{\tocsection {}{1}{Demo}}{1}{section.1}%
\contentsline {section}{\tocsection {}{2}{Introduction}}{1}{section.2}%
\contentsline {section}{\tocsection {}{3}{Discriminants of number fields}}{1}{section.3}%
\contentsline {section}{\tocsection {}{4}{Cyclotomic fields}}{4}{section.4}%
\contentsline {section}{\tocsection {}{5}{Fermat's Last Theorem for regular primes}}{5}{section.5}%
\contentsline {section}{\tocsection {}{1}{Introduction}}{1}{section.1}%
\contentsline {section}{\tocsection {}{2}{Discriminants of number fields}}{1}{section.2}%
\contentsline {section}{\tocsection {}{3}{Cyclotomic fields}}{4}{section.3}%
\contentsline {section}{\tocsection {}{4}{Fermat's Last Theorem for regular primes}}{5}{section.4}%
\contentsline {section}{\tocsection {}{}{References}}{8}{section*.2}%
3 changes: 1 addition & 2 deletions blueprint/src/content.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,9 @@

\home{https://leanprover-community.github.io/flt-regular/}
\github{https://github.com/leanprover-community/flt-regular/}
\dochome{https://cbirkbeck.github.io/FltRegulartest/doc/}

\maketitle

\section{Demo}
\label{cha:demo}

\input{demo}
2 changes: 1 addition & 1 deletion lake-manifest.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "be0d066cb7381532d79a03e56bfd664ecd6e69ba",
"rev": "a5516f580a31bf7ec20be84cc4fe50824cd3e35a",
"opts": {},
"name": "mathlib",
"inputRev?": null,
Expand Down

0 comments on commit 77ec1bc

Please sign in to comment.