bump

FltRegular/NumberTheory/Finrank.lean

@@ -16,36 +16,3 @@ instance torsion.module : Module R (M ⧸ AddCommGroup.torsion M) := by
   exact inferInstanceAs (Module R (M ⧸ this))
 
 end
-
-variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M)
-
-variable [Module.Finite R M]
-
-lemma FiniteDimensional.finrank_add_finrank_quotient [IsDomain R] (N : Submodule R M) :
-    finrank R (M ⧸ N) + finrank R N = finrank R M := by
-  rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
-    Submodule.finrank_eq_rank]
-  exact HasRankNullity.rank_quotient_add_rank _
-
-lemma FiniteDimensional.finrank_quotient [IsDomain R] (N : Submodule R M) :
-    finrank R (M ⧸ N) = finrank R M - finrank R N := by
-  rw [← FiniteDimensional.finrank_add_finrank_quotient N]
-  omega
-
-lemma FiniteDimensional.finrank_quotient' [IsDomain R] {S : Type*} [Ring S] [SMul R S] [Module S M]
-    [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N :=
-  FiniteDimensional.finrank_quotient (N.restrictScalars R)
-
-lemma FiniteDimensional.exists_of_finrank_lt [IsDomain R] (N : Submodule R M)
-    (h : finrank R N < finrank R M) : ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
-  obtain ⟨s, hs, hs'⟩ :=
-    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl
-  obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
-    hs, FiniteDimensional.finrank_quotient, tsub_eq_zero_iff_le, not_le]
-  obtain ⟨v, rfl⟩ := N.mkQ_surjective v
-  use v
-  intro r hr
-  have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
-  rw [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
-    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
-  exact mt this hr

FltRegular/NumberTheory/Hilbert92.lean

@@ -33,7 +33,7 @@ def systemOfUnits.isMaximal [Module.Finite ℤ G] (hf : finrank ℤ G = s * (p -
   apply Nonempty.some
   apply (@nonempty_fintype _ ?_)
   apply Module.finite_of_fg_torsion
-  rw [← finrank_eq_zero_iff_isTorsion, finrank_quotient',
+  rw [← finrank_eq_zero_iff_isTorsion, Submodule.finrank_quotient,
     finrank_spanA p hp _ _ sys.linearIndependent, hf, mul_comm, Nat.sub_self]
 
 noncomputable
@@ -693,7 +693,7 @@ lemma finrank_G : finrank ℤ G = (Units.rank k + 1) * (↑p - 1) := by
   refine (congr_arg Cardinal.toNat (rank_quotient_eq_of_le_torsion le_rfl)).trans ?_
   show finrank ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
     (MonoidHom.range <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))))) = _
-  rw [FiniteDimensional.finrank_quotient]
+  rw [Submodule.finrank_quotient]
   show _ - finrank ℤ (LinearMap.range <| AddMonoidHom.toIntLinearMap <|
     MonoidHom.toAdditive <| Units.map (algebraMap (𝓞 k) (𝓞 K) : (𝓞 k) →* (𝓞 K))) = _
   rw [LinearMap.finrank_range_of_inj, NumberField.Units.finrank_eq, NumberField.Units.finrank_eq,

FltRegular/NumberTheory/SystemOfUnits.lean

@@ -67,7 +67,7 @@ lemma ex_not_mem [Module.Free ℤ G] {R : ℕ} (S : systemOfUnits p G R) (hR : R
   have := Fact.mk hp
   have : Module.Finite ℤ G := Module.finite_of_finrank_pos
     (by simp [hf, R.zero_le.trans_lt hR, hp.one_lt])
-  refine FiniteDimensional.exists_of_finrank_lt
+  refine Submodule.exists_of_finrank_lt
     ((Submodule.span A (Set.range S.units)).restrictScalars ℤ) ?_
   show finrank ℤ (Submodule.span A _) < _
   rw [finrank_spanA p hp G S.units S.linearIndependent, hf, mul_comm]

lake-manifest.json

@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "03be989844769da3c80cae464d4ff2878b0494e7",
+   "rev": "9d502188e7df20d93aded2b312b28259ff1da308",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,