clean more stuff

FltRegular/CaseII/InductionStep.lean

@@ -121,14 +121,6 @@ lemma div_zeta_sub_one_Bijective :
     Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp]
   rfl
 
-/- if the image of one of the elements is zero then the corresponding x+yη is divisible by π^2-/
-lemma div_zeta_sub_one_eq_zero_iff (η) :
-    Ideal.Quotient.mk 𝔭 (div_zeta_sub_one hp hζ e η) = 0 ↔ π ^ 2 ∣ x + y * η := by
-  letI := IsCyclotomicExtension.numberField {p} ℚ K
-  rw [Ideal.Quotient.eq_zero_iff_dvd, pow_two,
-    ← div_zeta_sub_one_mul_zeta_sub_one hp hζ e,
-      mul_dvd_mul_iff_right (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]
-
 /- the gcd of x y called 𝔪 is coprime to 𝔭-/
 lemma gcd_zeta_sub_one_eq_one : gcd 𝔪 𝔭 = 1 := by
   have : Fact (Nat.Prime p) := hpri

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -78,12 +78,6 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K
   refine' Complex.norm_eq_one_of_pow_eq_one _ p.ne_zero
   rw [← map_pow, hζ.pow_eq_one, map_one]
 
--- this proof makes me happy inside
-theorem galConj_idempotent : (galConj K p).trans (galConj K p) = AlgEquiv.refl :=
-  by
-  rw [← AlgEquiv.aut_mul, galConj, ← map_mul, neg_one_mul, neg_neg, map_one]
-  rfl
-
 variable (p)
 
 --generalize this

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -33,15 +33,12 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) -
   apply RingHom.injective_int (algebraMap ℤ ℚ)
   simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp]
 
-@[simp]
-lemma PNat.coe_two : (2 : ℕ+) = (2 : ℕ) := rfl
-
 lemma surjective_of_isCyclotomicExtension_two (R S) [CommRing R] [CommRing S]
     [IsDomain S] [Algebra R S] [IsCyclotomicExtension {2} R S] :
     Function.Surjective (algebraMap R S) := by
   intro x
   have := IsCyclotomicExtension.adjoin_roots (S := {2}) (A := R) (B := S) x
-  simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.coe_two] at this
+  simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.val_ofNat] at this
   have H : Algebra.adjoin R {b : S | b = 1 ∨ b = -1} ≤ ⊥ := by
     rw [Algebra.adjoin_le_iff]
     rintro _ (rfl|rfl)
@@ -134,10 +131,6 @@ theorem prime_isUnit_mul {a b : α} (h : IsUnit a) : Prime (a * b) ↔ Prime b :
 
 theorem prime_mul_units (a : αˣ) (b : α) : Prime (b * ↑a) ↔ Prime b := by simp [Prime]
 
-theorem prime_mul_isUnit {a b : α} (h : IsUnit a) : Prime (b * a) ↔ Prime b :=
-  let ⟨a, ha⟩ := h
-  ha ▸ prime_mul_units a b
-
 theorem prime_neg_iff {α} [CommRing α] {a : α} : Prime (-a) ↔ Prime a := by
   rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg]
 

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -67,14 +67,6 @@ theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p := by
   rw [← this] at z1
   exact z1.of_map_of_injective (IsFractionRing.injective _ _)
 
-variable (p)
-
-/-- `is_gal_conj_real x` means that `x` is real. -/
-def IsGalConjReal (x : K) [IsCyclotomicExtension {p} ℚ K] : Prop :=
-  galConj K p x = x
-
-variable {p}
-
 theorem contains_two_primitive_roots {p q : ℕ} {x y : K} [FiniteDimensional ℚ K]
     (hx : IsPrimitiveRoot x p) (hy : IsPrimitiveRoot y q) :
     (lcm p q).totient ≤ FiniteDimensional.finrank ℚ K := by
@@ -307,11 +299,6 @@ theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h
   rw [sub_eq_of_eq_add hk] at this
   exact hζ.isPrime_one_sub_zeta.ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one)
 
-lemma IsUnit.eq_mul_left_iff {S : Type*} [CommRing S] {x : S} (hx : IsUnit x) (y : S) :
-  x = y * x ↔ y = 1 := by
-  nth_rw 1 [← one_mul x]
-  rw [eq_comm, hx.mul_left_injective.eq_iff]
-
 lemma map_two {S T F: Type*} [NonAssocSemiring S] [NonAssocSemiring T] [FunLike F S T]
   [RingHomClass F S T] (f : F) : f 2 = 2 := by
   rw [← one_add_one_eq_two, map_add, map_one]
@@ -403,13 +390,6 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
     · exact NumberField.RingOfIntegers.isIntegral_coe _
   · exact unit_lemma_val_one p u
 
-lemma inv_coe_coe {K A : Type*} [Field K] [SetLike A K] [SubsemiringClass A K] {S : A} (s : Sˣ) :
-  (s : K)⁻¹ = ((s⁻¹ : Sˣ) : K) := by
-  apply inv_eq_of_mul_eq_one_right
-  change ((s * s⁻¹ : Sˣ) : K) = 1
-  rw [mul_inv_self]
-  rfl
-
 lemma IsPrimitiveRoot.eq_one_mod_one_sub' {A : Type*} [CommRing A] [IsDomain A]
     {n : ℕ+} {ζ : A} (hζ : IsPrimitiveRoot ζ n) {η : A} (hη : η ∈ nthRootsFinset n A) :
     Ideal.Quotient.mk (Ideal.span ({ζ - 1} : Set A)) η = 1 := by

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -222,14 +222,6 @@ lemma minpoly_polyRoot' {L : Type*} [Field L] [Algebra K L] (α : L)
   exact minpoly_polyRoot'' hp hζ u hcong hu α e i
   exact IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop
 
-lemma minpoly_polyRoot {L : Type*} [Field L] [Algebra K L] (α : L)
-    (e : α ^ (p : ℕ) = algebraMap K L u) (i) :
-    minpoly (𝓞 K) (polyRoot hp hζ u hcong α e i) = (poly hp hζ u hcong) := by
-  apply map_injective (algebraMap (𝓞 K) K) Subtype.coe_injective
-  rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L]
-  exact minpoly_polyRoot'' hp hζ u hcong hu α e i
-  exact IsIntegralClosure.isIntegral _ L (polyRoot hp hζ u hcong α e i)
-
 lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) : Separable ((poly hp hζ u hcong).map
     (algebraMap (𝓞 K) (𝓞 L))) := by

FltRegular/NumberTheory/SystemOfUnits.lean

@@ -35,29 +35,9 @@ structure systemOfUnits (r : ℕ)
 
 namespace systemOfUnits
 
-lemma nontrivial (hr : r ≠ 0) : Nontrivial G := by
-    by_contra! h
-    rw [not_nontrivial_iff_subsingleton] at h
-    rw [FiniteDimensional.finrank_zero_of_subsingleton] at hf
-    simp only [ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf
-    cases hf with
-    | inl h => exact hr h
-    | inr h => simpa [Nat.lt_succ_iff, h] using not_lt.2 (Nat.prime_def_lt.1 hp).1
-
 lemma existence0 : Nonempty (systemOfUnits p G 0) := by
     exact ⟨⟨fun _ => 0, linearIndependent_empty_type⟩⟩
 
-lemma spanA_eq_spanZ {R : ℕ} (f : Fin R → G) :
-    (Submodule.span A (Set.range f)).restrictScalars ℤ = Submodule.span ℤ
-      (Set.range (fun (e : Fin R × (Fin (p - 1))) ↦ (zeta p) ^ e.2.1 • f e.1)) := by
-  letI := Fact.mk hp
-  rw [← Submodule.span_smul_of_span_eq_top (CyclotomicIntegers.powerBasis p).basis.span_eq,
-    Set.range_smul_range]
-  congr
-  ext
-  simp only [PowerBasis.coe_basis, CyclotomicIntegers.powerBasis_gen, Set.mem_range, Prod.exists]
-  rw [exists_comm, CyclotomicIntegers.powerBasis_dim]
-
 theorem _root_.PowerBasis.finrank' {R S} [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S]
     (pb : PowerBasis R S) : FiniteDimensional.finrank R S = pb.dim := by
   rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin]

FltRegular/ReadyForMathlib/PowerBasis.lean

@@ -47,19 +47,10 @@ variable [NumberField K] {pb}
 
 variable (hpr : Prime (norm ℚ pb.gen))
 
-theorem quotient_not_trivial : Nontrivial ((𝓞 K) ⧸ span ({pb.gen} : Set (𝓞 K))) :=
-  Quotient.nontrivial fun h => hpr.not_unit ((isUnit_norm ℚ).2 (span_singleton_eq_top.1 h))
-
 lemma SModEq.Ideal_def {R : Type*} [CommRing R] (I : Ideal R) (x y : R) :
   x ≡ y [SMOD I] ↔ Ideal.Quotient.mk I x = Ideal.Quotient.mk I y :=
 Iff.rfl
 
-instance {K : Type*} [Field K] [NumberField K] :
-  Module (𝓞 ℚ) (𝓞 K) := Algebra.toModule
-
-instance {K : Type*} [Field K] [NumberField K] :
-  SMul (𝓞 ℚ) (𝓞 K) := Algebra.toSMul
-
 lemma norm_intCast {K : Type*} [Field K] [NumberField K] (n : ℤ) :
   norm ℚ (n : 𝓞 K) = n ^ (finrank ℚ K) := by
   rw [← eq_intCast (algebraMap ℤ (𝓞 K)) n, IsScalarTower.algebraMap_apply ℤ (𝓞 ℚ) (𝓞 K)]