deploy: 819c838

leanprover-community · Jan 2, 2023 · 6d01f71 · 6d01f71
1 parent b031f45
commit 6d01f71
Show file tree

Hide file tree

Showing 8 changed files with 57 additions and 60 deletions.
diff --git a/blueprint.pdf b/blueprint.pdf
diff --git a/dep_graph_document.html b/dep_graph_document.html
diff --git a/sect0002.html b/sect0002.html
@@ -75,7 +75,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/norm.lean#L279">algebra.norm_eq_prod_embeddings</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/norm.lean#L279">algebra.norm_eq_prod_embeddings</a></li>
         </ul>
 
       </div>
@@ -124,7 +124,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/trace.lean#L349">trace_eq_sum_embeddings</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/trace.lean#L349">trace_eq_sum_embeddings</a></li>
         </ul>
 
       </div>
@@ -170,7 +170,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L65">algebra.discr</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L65">algebra.discr</a></li>
         </ul>
 
       </div>
@@ -238,7 +238,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L124">algebra.discr_not_zero_of_basis</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L124">algebra.discr_not_zero_of_basis</a></li>
         </ul>
 
       </div>
@@ -298,7 +298,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L110">algebra.discr_of_matrix_mul_vec</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L110">algebra.discr_of_matrix_mul_vec</a></li>
         </ul>
 
       </div>
@@ -362,7 +362,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L146">algebra.discr_eq_det_embeddings_matrix_reindex_pow_two</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L146">algebra.discr_eq_det_embeddings_matrix_reindex_pow_two</a></li>
         </ul>
 
       </div>
@@ -449,7 +449,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L153">algebra.discr_power_basis_eq_prod</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L153">algebra.discr_power_basis_eq_prod</a></li>
         </ul>
 
       </div>
@@ -526,7 +526,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/data/polynomial/splits.lean#L375">polynomial.aeval_root_derivative_of_splits</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/data/polynomial/splits.lean#L375">polynomial.aeval_root_derivative_of_splits</a></li>
         </ul>
 
       </div>
@@ -596,7 +596,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L207">algebra.discr_power_basis_eq_norm</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L207">algebra.discr_power_basis_eq_norm</a></li>
         </ul>
 
       </div>
@@ -653,7 +653,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/norm.lean#L304">algebra.is_integral_norm</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/norm.lean#L304">algebra.is_integral_norm</a></li>
         </ul>
 
       </div>
@@ -698,7 +698,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/trace.lean#L286">algebra.is_integral_trace</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/trace.lean#L286">algebra.is_integral_trace</a></li>
         </ul>
 
       </div>
@@ -759,7 +759,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L267">algebra.discr_is_integral</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L267">algebra.discr_is_integral</a></li>
         </ul>
 
       </div>
@@ -820,7 +820,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/discriminant.lean#L313">algebra.discr_mul_is_integral_mem_adjoin</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/discriminant.lean#L313">algebra.discr_mul_is_integral_mem_adjoin</a></li>
         </ul>
 
       </div>
@@ -881,7 +881,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/polynomial/eisenstein.lean#L584">mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/polynomial/eisenstein.lean#L584">mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at</a></li>
         </ul>
 
       </div>

diff --git a/sect0003.html b/sect0003.html
@@ -74,7 +74,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/polynomial/cyclotomic/basic.lean#L339">polynomial.degree_cyclotomic</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/polynomial/cyclotomic/basic.lean#L339">polynomial.degree_cyclotomic</a></li>
         </ul>
 
       </div>
@@ -119,7 +119,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/ring_theory/polynomial/cyclotomic/basic.lean#L832">polynomial.cyclotomic.irreducible</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/ring_theory/polynomial/cyclotomic/basic.lean#L832">polynomial.cyclotomic.irreducible</a></li>
         </ul>
 
       </div>
@@ -181,7 +181,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/mathlib/blob/a437a2499163d85d670479f69f625f461cc5fef9/src/number_theory/cyclotomic/rat.lean#L56">is_cyclotomic_extension.rat.discr_prime_pow'</a></li>
+          <li><a href="https://github.com/leanprover-community/mathlib/blob/1e05171a5e8cf18d98d9cf7b207540acb044acae/src/number_theory/cyclotomic/rat.lean#L56">is_cyclotomic_extension.rat.discr_prime_pow'</a></li>
         </ul>
 
       </div>
@@ -358,7 +358,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/cyclotomic/Unit_lemmas.lean#L283">roots_of_unity_in_cyclo</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/cyclotomic/Unit_lemmas.lean#L283">roots_of_unity_in_cyclo</a></li>
         </ul>
 
       </div>
@@ -419,7 +419,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/cyclotomic/Unit_lemmas.lean#L450">unit_lemma_gal_conj</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/cyclotomic/Unit_lemmas.lean#L450">unit_lemma_gal_conj</a></li>
         </ul>
 
       </div>

diff --git a/sect0004.html b/sect0004.html
@@ -89,7 +89,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/cyclotomic/cycl_rat.lean#L387">flt_ideals_coprime</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/cyclotomic/cycl_rat.lean#L387">flt_ideals_coprime</a></li>
         </ul>
 
       </div>
@@ -143,7 +143,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/cyclotomic/cycl_rat.lean#L27">exists_int_sub_pow_prime_dvd</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/cyclotomic/cycl_rat.lean#L27">exists_int_sub_pow_prime_dvd</a></li>
         </ul>
 
       </div>
@@ -188,7 +188,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/cyclotomic/cycl_rat.lean#L449">dvd_coeff_cycl_integer</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/cyclotomic/cycl_rat.lean#L449">dvd_coeff_cycl_integer</a></li>
         </ul>
 
       </div>
@@ -298,7 +298,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/caseI/statement.lean#L28">flt_regular.caseI.may_assume</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/caseI/statement.lean#L28">flt_regular.caseI.may_assume</a></li>
         </ul>
 
       </div>
@@ -355,7 +355,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/regular_primes.lean#L51">is_regular_number</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/regular_primes.lean#L51">is_regular_number</a></li>
         </ul>
 
       </div>
@@ -407,7 +407,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/caseI/statement.lean#L271">flt_regular.caseI</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/caseI/statement.lean#L271">flt_regular.caseI</a></li>
         </ul>
 
       </div>
@@ -459,7 +459,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/number_theory/kummers_lemma.lean#L17">eq_pow_prime_of_unit_of_congruent</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/number_theory/kummers_lemma.lean#L17">eq_pow_prime_of_unit_of_congruent</a></li>
         </ul>
 
       </div>
@@ -613,7 +613,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/caseII/statement.lean#L11">flt_regular.caseII</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/caseII/statement.lean#L11">flt_regular.caseII</a></li>
         </ul>
 
       </div>
@@ -664,7 +664,7 @@ <h1>Lean declarations</h1>
 </button>
         </header>
                 <ul class="uses">
-          <li><a href="https://github.com/leanprover-community/flt-regular//blob/1431c9757156c60fa6e21a2ea982c5bdd52397a2/src/flt_regular.lean#L12">flt_regular</a></li>
+          <li><a href="https://github.com/leanprover-community/flt-regular//blob/819c8381c1316a98c573e38511fea53fc0b53aaa/src/flt_regular.lean#L12">flt_regular</a></li>
         </ul>
 
       </div>