mini improvements

leanprover-community · Jul 24, 2024 · c7381e2 · c7381e2
1 parent e64d2e0
commit c7381e2
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 7 deletions.
diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean
@@ -461,7 +461,7 @@ lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
   rw [this.resolve_left (pow_ne_zero (m + 1) (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt))] at hz
   exact hz (dvd_zero _)
 
-lemma stuff (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀) :
+lemma formula (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀) :
   (η₂ - η₀ : 𝓞 K) * ε η₁ hη₁ * (α η₁ hη₁ * β η₂ hη₂) ^ (p : ℕ) +
     (η₀ - η₁) * ε η₂ hη₂ * (α η₂ hη₂ * β η₁ hη₁) ^ (p : ℕ) =
     (η₂ - η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ (p : ℕ) := by
@@ -508,7 +508,7 @@ lemma exists_solution :
     (Subtype.coe_injective.ne_iff.mpr hη₁.symm)
   obtain ⟨u₃, hu₃⟩ := hζ.unit'_coe.associated_sub_one hpri.out η₂.prop (η₁ : _).prop
     (Subtype.coe_injective.ne_iff.mpr hη)
-  have := stuff hp hreg hζ e hy hz η₁ hη₁ η₂ hη₂
+  have := formula hp hreg hζ e hy hz η₁ hη₁ η₂ hη₂
   rw [← hu₁, ← hu₂, ← hu₃, mul_assoc _ (u₁ : 𝓞 K), mul_assoc _ (u₂ : 𝓞 K), mul_assoc _ (u₃ : 𝓞 K),
     mul_assoc (π), mul_assoc (π), ← mul_add,
     mul_right_inj' (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt), ← Units.val_mul,

diff --git a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean b/FltRegular/NumberTheory/Cyclotomic/Factoring.lean
@@ -16,8 +16,7 @@ open Polynomial Finset MvPolynomial
 where `μ` varies over the `n`-th roots of unity. -/
 theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type _} [CommRing K] [IsDomain K] {ζ : K}
     {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) (x y : K) :
-    x ^ (n : ℕ) - y ^ (n : ℕ) = ∏ ζ : K in nthRootsFinset n K, (x - ζ * y) :=
-  by
+    x ^ (n : ℕ) - y ^ (n : ℕ) = ∏ ζ : K in nthRootsFinset n K, (x - ζ * y) := by
   -- suffices to show the identity in a multivariate polynomial ring with two generators over K
   suffices
     (X 0 : MvPolynomial (Fin 2) K) ^ (n : ℕ) - X 1 ^ (n : ℕ) =

diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean
@@ -18,8 +18,8 @@ variable [IsSplittingField K L (X ^ (p : ℕ) - C (u : K))]
 variable (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowers σ)
 
 theorem false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne (u : (𝓞 K)ˣ)
-    (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1)
-    (hu : ∀ v : K, v ^ (p : ℕ) ≠ u) : False := by
+    (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) : ¬∀ v : K, v ^ (p : ℕ) ≠ u := by
+  intro hu
   letI := Fact.mk (X_pow_sub_C_irreducible_of_prime hpri.out hu)
   let L := AdjoinRoot (Polynomial.X ^ (p : ℕ) - Polynomial.C (u : K))
   haveI := isSplittingField_AdjoinRoot_X_pow_sub_C ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩
@@ -75,7 +75,7 @@ theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ)
     simpa [ge_iff_le, Int.cast_one, sub_self, nsmul_eq_mul, Nat.cast_mul, PNat.pos,
       Nat.cast_pred, zero_sub, IsUnit.mul_iff, ne_eq, tsub_eq_zero_iff_le, not_le, dvd_neg,
       Units.isUnit, and_true, zero_add] using this
-  have : ¬(∀ v : K, _) := false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne hp hreg hζ _ this
+  have := false_of_zeta_sub_one_pow_dvd_sub_one_of_pow_ne hp hreg hζ _ this
   simp only [not_forall, not_not] at this
   obtain ⟨v, hv⟩ := this
   have hv' : IsIntegral ℤ v := by