bump

leanprover-community · Jul 15, 2024 · 53ee391 · 53ee391
1 parent c507e4d
commit 53ee391
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 9 deletions.
diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean
@@ -324,11 +324,6 @@ theorem obscure' (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity
           simp [haparity, hbparity, three_ne_zero, parity_simps]
         tauto
 
-theorem Int.eq_pow_of_mul_eq_pow_odd {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k)
-    (h : a * b = c ^ k) : (∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k := by
-  obtain ⟨k, rfl⟩ := hk.exists_bit1
-  exact Int.eq_pow_of_mul_eq_pow_bit1 hab h
-
 theorem Int.cube_of_coprime (a b c s : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0)
     (hcoprimeab : IsCoprime a b) (hcoprimeac : IsCoprime a c) (hcoprimebc : IsCoprime b c)
     (hs : a * b * c = s ^ 3) : ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3 :=

diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -427,3 +427,5 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
   obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.cast hdim.symm) ⟨j, hj⟩) y m
   rw [hy, ← smul_eq_mul, ← zsmul_eq_smul_cast, ← b.basis.coord_apply, ← Fin.cast_mk, hn]
   exact dvd_add (dvd_mul_right _ _) last_dvd
+
+end IntFacts
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean b/FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean
@@ -152,3 +152,5 @@ lemma IsPrimitiveRoot.associated_sub_one {A : Type*} [CommRing A] [IsDomain A]
   rw [h, associated_isUnit_mul_right_iff u.isUnit, ← associated_isUnit_mul_right_iff isUnit_one.neg,
     neg_one_mul, neg_sub]
   rfl
+
+end CyclotomicUnit
diff --git a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean b/FltRegular/NumberTheory/Cyclotomic/Factoring.lean
@@ -30,7 +30,7 @@ theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type _} [CommRing K] [IsDom
   -- transfer this to a polynomial ring with two variables
   have := congr_arg (Polynomial.aeval (X 0 : MvPolynomial (Fin 2) K)) this
   simp only [map_prod, aeval_X_pow, Polynomial.aeval_X, aeval_one, Polynomial.aeval_C,
-    AlgHom.map_sub] at this
+    map_sub] at this
   -- the homogenization of the identity is also true
   have := congr_arg (homogenization 1) this
   -- simplify to get the result we want

diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -396,7 +396,7 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p.
     rw [← Finset.filter_val, ← Finset.card, ← Fintype.card_subtype]
     obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq (L ≃ₐ[K] L) P ⟨P', hP'⟩
     have : P' = ↑(σ • P) := by rw [hσ]
-    simp_rw [this, ← Subtype.ext_iff, ← eq_inv_smul_iff (a := σ), ← mul_smul, eq_comm (a := P)]
+    simp_rw [this, ← Subtype.ext_iff, ← eq_inv_smul_iff (g := σ), ← mul_smul, eq_comm (a := P)]
     exact Fintype.card_congr
       { toFun := fun x ↦ ⟨σ⁻¹ * x, x.prop⟩,
         invFun := fun x ↦ ⟨σ * x, (inv_mul_cancel_left σ x).symm ▸ x.prop⟩,

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "529a610e12f52837fbd7a977b288cbe7ab5b86bb",
+   "rev": "08bbfd6e4f66aaf6d3ef8e23fb18903707d1f14b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,