Trigger CI for leanprover-community/batteries#1063

Archive/Hairer.lean

@@ -26,6 +26,7 @@ noncomputable section
 open Metric Set MeasureTheory
 open MvPolynomial hiding support
 open Function hiding eval
+open scoped ContDiff
 
 variable {ι : Type*} [Fintype ι]
 
@@ -110,7 +111,7 @@ lemma inj_L : Injective (L ι) :=
     apply subset_closure
 
 lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
-    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
+    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ∞ ρ ∧
     ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →
     ∫ x : EuclideanSpace ℝ ι, eval x p • ρ x = eval 0 p := by
   have := (inj_L ι).comp (restrictTotalDegree ι ℝ N).injective_subtype

Counterexamples/DirectSumIsInternal.lean

@@ -12,10 +12,10 @@ import Mathlib.Tactic.FinCases
 # Not all complementary decompositions of a module over a semiring make up a direct sum
 
 This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
-implies as a collection they are `CompleteLattice.Independent` and that they span all of `ℤ`, they
+implies as a collection they are `iSupIndep` and that they span all of `ℤ`, they
 do not form a decomposition into a direct sum.
 
-This file demonstrates why `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top` must
+This file demonstrates why `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` must
 take `Ring R` and not `Semiring R`.
 -/
 
@@ -57,9 +57,9 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
     · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
     · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 
-def withSign.independent : CompleteLattice.Independent withSign := by
+def withSign.independent : iSupIndep withSign := by
   apply
-    (CompleteLattice.independent_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
+    (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i
   fin_cases i <;> simp
 

Mathlib.lean

@@ -2449,6 +2449,7 @@ import Mathlib.Data.Finsupp.Fintype
 import Mathlib.Data.Finsupp.Indicator
 import Mathlib.Data.Finsupp.Interval
 import Mathlib.Data.Finsupp.Lex
+import Mathlib.Data.Finsupp.MonomialOrder
 import Mathlib.Data.Finsupp.Multiset
 import Mathlib.Data.Finsupp.NeLocus
 import Mathlib.Data.Finsupp.Notation
@@ -3918,6 +3919,7 @@ import Mathlib.Order.CompletePartialOrder
 import Mathlib.Order.CompleteSublattice
 import Mathlib.Order.Concept
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Order.ConditionallyCompleteLattice.Defs
 import Mathlib.Order.ConditionallyCompleteLattice.Finset
 import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Order.ConditionallyCompleteLattice.Indexed
@@ -4322,6 +4324,7 @@ import Mathlib.RingTheory.LaurentSeries
 import Mathlib.RingTheory.LinearDisjoint
 import Mathlib.RingTheory.LittleWedderburn
 import Mathlib.RingTheory.LocalProperties.Basic
+import Mathlib.RingTheory.LocalProperties.Exactness
 import Mathlib.RingTheory.LocalProperties.IntegrallyClosed
 import Mathlib.RingTheory.LocalProperties.Projective
 import Mathlib.RingTheory.LocalProperties.Reduced

Mathlib/Algebra/DirectSum/Basic.lean

@@ -367,8 +367,8 @@ theorem coe_of_apply {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S
 `M` is said to be internal if the canonical map `(⨁ i, A i) →+ M` is bijective.
 
 For the alternate statement in terms of independence and spanning, see
-`DirectSum.subgroup_isInternal_iff_independent_and_supr_eq_top` and
-`DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top`. -/
+`DirectSum.subgroup_isInternal_iff_iSupIndep_and_supr_eq_top` and
+`DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top`. -/
 def IsInternal {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
     [AddSubmonoidClass S M] (A : ι → S) : Prop :=
   Function.Bijective (DirectSum.coeAddMonoidHom A)

Mathlib/Algebra/DirectSum/Internal.lean

@@ -28,7 +28,7 @@ to represent this case, `(h : DirectSum.IsInternal A) [SetLike.GradedMonoid A]`
 needed. In the future there will likely be a data-carrying, constructive, typeclass version of
 `DirectSum.IsInternal` for providing an explicit decomposition function.
 
-When `CompleteLattice.Independent (Set.range A)` (a weaker condition than
+When `iSupIndep (Set.range A)` (a weaker condition than
 `DirectSum.IsInternal A`), these provide a grading of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
 `DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)`.

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -82,8 +82,8 @@ lemma trace_eq_zero_of_mapsTo_ne (h : IsInternal N) [IsNoetherian R M]
     (σ : ι → ι) (hσ : ∀ i, σ i ≠ i) {f : Module.End R M}
     (hf : ∀ i, MapsTo f (N i) (N <| σ i)) :
     trace R M f = 0 := by
-  have hN : {i | N i ≠ ⊥}.Finite := CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent
-    h.submodule_independent
+  have hN : {i | N i ≠ ⊥}.Finite := WellFoundedGT.finite_ne_bot_of_iSupIndep
+    h.submodule_iSupIndep
   let s := hN.toFinset
   let κ := fun i ↦ Module.Free.ChooseBasisIndex R (N i)
   let b : (i : s) → Basis (κ i) R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)
@@ -109,10 +109,10 @@ lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
       (f.mapsTo_maxGenEigenspace_of_comm rfl μ)
   suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
     classical
-    have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
+    have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
       f.independent_maxGenEigenspace hf
     have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
-      CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent f.independent_maxGenEigenspace
+      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace
     simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
   intro μ
   replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
@@ -136,14 +136,14 @@ Note that it is important the statement gives the user definitional control over
 _type_ of the term `trace R p (f.restrict hp')` depends on `p`. -/
 lemma trace_eq_sum_trace_restrict_of_eq_biSup
     [∀ i, Module.Finite R (N i)] [∀ i, Module.Free R (N i)]
-    (s : Finset ι) (h : CompleteLattice.Independent <| fun i : s ↦ N i)
+    (s : Finset ι) (h : iSupIndep <| fun i : s ↦ N i)
     {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i))
     (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
     (hp' : MapsTo f p p := hp ▸ mapsTo_biSup_of_mapsTo (s : Set ι) hf) :
     trace R p (f.restrict hp') = ∑ i ∈ s, trace R (N i) (f.restrict (hf i)) := by
   classical
   let N' : s → Submodule R p := fun i ↦ (N i).comap p.subtype
-  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_independent (s : Set ι) h
+  replace h : IsInternal N' := hp ▸ isInternal_biSup_submodule_of_iSupIndep (s : Set ι) h
   have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using hf i hx'
   let e : (i : s) → N' i ≃ₗ[R] N i := fun ⟨i, hi⟩ ↦ (N i).comapSubtypeEquivOfLe (hp ▸ le_biSup N hi)
   have _i1 : ∀ i, Module.Finite R (N' i) := fun i ↦ Module.Finite.equiv (e i).symm

Mathlib/Algebra/DirectSum/Module.lean

@@ -319,8 +319,11 @@ theorem IsInternal.submodule_iSup_eq_top (h : IsInternal A) : iSup A = ⊤ := by
   exact Function.Bijective.surjective h
 
 /-- If a direct sum of submodules is internal then the submodules are independent. -/
-theorem IsInternal.submodule_independent (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_lsum_injective _ h.injective
+theorem IsInternal.submodule_iSupIndep (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_lsum_injective _ h.injective
+
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.submodule_independent := IsInternal.submodule_iSupIndep
 
 /-- Given an internal direct sum decomposition of a module `M`, and a basis for each of the
 components of the direct sum, the disjoint union of these bases is a basis for `M`. -/
@@ -374,7 +377,7 @@ the two submodules are complementary. Over a `Ring R`, this is true as an iff, a
 `DirectSum.isInternal_submodule_iff_isCompl`. -/
 theorem IsInternal.isCompl {A : ι → Submodule R M} {i j : ι} (hij : i ≠ j)
     (h : (Set.univ : Set ι) = {i, j}) (hi : IsInternal A) : IsCompl (A i) (A j) :=
-  ⟨hi.submodule_independent.pairwiseDisjoint hij,
+  ⟨hi.submodule_iSupIndep.pairwiseDisjoint hij,
     codisjoint_iff.mpr <| Eq.symm <| hi.submodule_iSup_eq_top.symm.trans <| by
       rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]⟩
 
@@ -387,60 +390,76 @@ variable {ι : Type v} [dec_ι : DecidableEq ι]
 variable {M : Type*} [AddCommGroup M] [Module R M]
 
 /-- Note that this is not generally true for `[Semiring R]`; see
-`CompleteLattice.Independent.dfinsupp_lsum_injective` for details. -/
-theorem isInternal_submodule_of_independent_of_iSup_eq_top {A : ι → Submodule R M}
-    (hi : CompleteLattice.Independent A) (hs : iSup A = ⊤) : IsInternal A :=
+`iSupIndep.dfinsupp_lsum_injective` for details. -/
+theorem isInternal_submodule_of_iSupIndep_of_iSup_eq_top {A : ι → Submodule R M}
+    (hi : iSupIndep A) (hs : iSup A = ⊤) : IsInternal A :=
   ⟨hi.dfinsupp_lsum_injective,
     -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify value of `f`
     (LinearMap.range_eq_top (f := DFinsupp.lsum _ _)).1 <|
       (Submodule.iSup_eq_range_dfinsupp_lsum _).symm.trans hs⟩
 
-/-- `iff` version of `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top`,
-`DirectSum.IsInternal.submodule_independent`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
-theorem isInternal_submodule_iff_independent_and_iSup_eq_top (A : ι → Submodule R M) :
-    IsInternal A ↔ CompleteLattice.Independent A ∧ iSup A = ⊤ :=
-  ⟨fun i ↦ ⟨i.submodule_independent, i.submodule_iSup_eq_top⟩,
-    And.rec isInternal_submodule_of_independent_of_iSup_eq_top⟩
+@[deprecated (since := "2024-11-24")]
+alias isInternal_submodule_of_independent_of_iSup_eq_top :=
+  isInternal_submodule_of_iSupIndep_of_iSup_eq_top
+
+/-- `iff` version of `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top`,
+`DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`. -/
+theorem isInternal_submodule_iff_iSupIndep_and_iSup_eq_top (A : ι → Submodule R M) :
+    IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤ :=
+  ⟨fun i ↦ ⟨i.submodule_iSupIndep, i.submodule_iSup_eq_top⟩,
+    And.rec isInternal_submodule_of_iSupIndep_of_iSup_eq_top⟩
+
+@[deprecated (since := "2024-11-24")]
+alias isInternal_submodule_iff_independent_and_iSup_eq_top :=
+  isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
 
 /-- If a collection of submodules has just two indices, `i` and `j`, then
 `DirectSum.IsInternal` is equivalent to `isCompl`. -/
 theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j)
     (h : (Set.univ : Set ι) = {i, j}) : IsInternal A ↔ IsCompl (A i) (A j) := by
   have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
-  rw [isInternal_submodule_iff_independent_and_iSup_eq_top, iSup, ← Set.image_univ, h,
-    Set.image_insert_eq, Set.image_singleton, sSup_pair, CompleteLattice.independent_pair hij this]
+  rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h,
+    Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]
   exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
 
 @[simp]
 theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
     IsInternal (fun i : {i // A i ≠ ⊥} ↦ A i) ↔ IsInternal A := by
-  simp only [isInternal_submodule_iff_independent_and_iSup_eq_top]
-  exact Iff.and CompleteLattice.independent_ne_bot_iff_independent <| by simp
+  simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]
 
-lemma isInternal_biSup_submodule_of_independent {A : ι → Submodule R M} (s : Set ι)
-    (h : CompleteLattice.Independent <| fun i : s ↦ A i) :
+lemma isInternal_biSup_submodule_of_iSupIndep {A : ι → Submodule R M} (s : Set ι)
+    (h : iSupIndep <| fun i : s ↦ A i) :
     IsInternal <| fun (i : s) ↦ (A i).comap (⨆ i ∈ s, A i).subtype := by
-  refine (isInternal_submodule_iff_independent_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
+  refine (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
   let p := ⨆ i ∈ s, A i
   have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
   let e : Submodule R p ≃o Set.Iic p := p.mapIic
   suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
-    rw [← CompleteLattice.independent_map_orderIso_iff e, this]
-    exact CompleteLattice.independent_of_independent_coe_Iic_comp h
+    rw [← iSupIndep_map_orderIso_iff e, this]
+    exact .of_coe_Iic_comp h
   ext i m
   change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
   rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
 
+@[deprecated (since := "2024-11-24")]
+alias isInternal_biSup_submodule_of_independent := isInternal_biSup_submodule_of_iSupIndep
+
 /-! Now copy the lemmas for subgroup and submonoids. -/
 
 
-theorem IsInternal.addSubmonoid_independent {M : Type*} [AddCommMonoid M] {A : ι → AddSubmonoid M}
-    (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_sumAddHom_injective _ h.injective
+theorem IsInternal.addSubmonoid_iSupIndep {M : Type*} [AddCommMonoid M] {A : ι → AddSubmonoid M}
+    (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_sumAddHom_injective _ h.injective
+
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.addSubmonoid_independent := IsInternal.addSubmonoid_iSupIndep
+
+theorem IsInternal.addSubgroup_iSupIndep {G : Type*} [AddCommGroup G] {A : ι → AddSubgroup G}
+    (h : IsInternal A) : iSupIndep A :=
+  iSupIndep_of_dfinsupp_sumAddHom_injective' _ h.injective
 
-theorem IsInternal.addSubgroup_independent {M : Type*} [AddCommGroup M] {A : ι → AddSubgroup M}
-    (h : IsInternal A) : CompleteLattice.Independent A :=
-  CompleteLattice.independent_of_dfinsupp_sumAddHom_injective' _ h.injective
+@[deprecated (since := "2024-11-24")]
+alias IsInternal.addSubgroup_independent := IsInternal.addSubgroup_iSupIndep
 
 end Ring
 

Mathlib/Algebra/DirectSum/Ring.lean

@@ -63,9 +63,8 @@ instances for:
 * `A : ι → Submodule S`:
   `DirectSum.GSemiring.ofSubmodules`, `DirectSum.GCommSemiring.ofSubmodules`.
 
-If `CompleteLattice.independent (Set.range A)`, these provide a gradation of `⨆ i, A i`, and the
-mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as
-`DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)`.
+If `sSupIndep A`, these provide a gradation of `⨆ i, A i`, and the mapping `⨁ i, A i →+ ⨆ i, A i`
+can be obtained as `DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion <| le_iSup A i)`.
 
 ## Tags
 

Mathlib/Algebra/Group/Pointwise/Set/Card.lean

@@ -38,7 +38,7 @@ lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
 end Mul
 
 section InvolutiveInv
-variable [InvolutiveInv G] {s t : Set G}
+variable [InvolutiveInv G]
 
 @[to_additive (attr := simp)]
 lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by

Mathlib/Algebra/GroupWithZero/Pointwise/Set/Card.lean

@@ -13,7 +13,7 @@ import Mathlib.SetTheory.Cardinal.Finite
 
 open scoped Cardinal Pointwise
 
-variable {G G₀ M M₀ : Type*}
+variable {G₀ M₀ : Type*}
 
 namespace Set
 variable [GroupWithZero G₀] [Zero M₀] [MulActionWithZero G₀ M₀] {a : G₀}

Mathlib/Algebra/Homology/Additive.lean

@@ -23,8 +23,8 @@ variable {ι : Type*}
 variable {V : Type u} [Category.{v} V] [Preadditive V]
 variable {W : Type*} [Category W] [Preadditive W]
 variable {W₁ W₂ : Type*} [Category W₁] [Category W₂] [HasZeroMorphisms W₁] [HasZeroMorphisms W₂]
-variable {c : ComplexShape ι} {C D E : HomologicalComplex V c}
-variable (f g : C ⟶ D) (h k : D ⟶ E) (i : ι)
+variable {c : ComplexShape ι} {C D : HomologicalComplex V c}
+variable (f : C ⟶ D) (i : ι)
 
 namespace HomologicalComplex
 

Mathlib/Algebra/Lie/Semisimple/Basic.lean

@@ -147,7 +147,7 @@ lemma isSimple_of_isAtom (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I where
         -- Finally `⁅b, y⁆ = 0`, by the independence of the atoms.
         · suffices ⁅b, y.val⁆ = 0 by erw [this]; simp only [zero_mem]
           rw [← LieSubmodule.mem_bot (R := R) (L := L),
-              ← (IsSemisimple.setIndependent_isAtom hI).eq_bot]
+              ← (IsSemisimple.sSupIndep_isAtom hI).eq_bot]
           exact ⟨lie_mem_right R L I b y y.2, lie_mem_left _ _ _ _ _ hb⟩ }
     -- Now that we know that `J` is an ideal of `L`,
     -- we start with the proof that `I` is a simple Lie algebra.
@@ -240,7 +240,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal
   constructor
   -- `j` brackets to `0` with `z`, since `⁅j, z⁆` is contained in `⁅J, K⁆ ≤ J ⊓ K`,
   -- and `J ⊓ K = ⊥` by the independence of the atoms.
-  · apply (setIndependent_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.not_mem_erase _ _)).le_bot
+  · apply (sSupIndep_isAtom.disjoint_sSup (hs hJs) hs'S (Finset.not_mem_erase _ _)).le_bot
     apply LieSubmodule.lie_le_inf
     apply LieSubmodule.lie_mem_lie j.2
     simpa only [K, Finset.sup_id_eq_sSup] using hz
@@ -292,7 +292,7 @@ instance (priority := 100) IsSimple.instIsSemisimple [IsSimple R L] :
     IsSemisimple R L := by
   constructor
   · simp
-  · simpa using CompleteLattice.setIndependent_singleton _
+  · simpa using sSupIndep_singleton _
   · intro I hI₁ hI₂
     apply IsSimple.non_abelian (R := R) (L := L)
     rw [IsSimple.isAtom_iff_eq_top] at hI₁

Mathlib/Algebra/Lie/Semisimple/Defs.lean

@@ -72,7 +72,7 @@ class IsSemisimple : Prop where
   /-- In a semisimple Lie algebra, the supremum of the atoms is the whole Lie algebra. -/
   sSup_atoms_eq_top : sSup {I : LieIdeal R L | IsAtom I} = ⊤
   /-- In a semisimple Lie algebra, the atoms are independent. -/
-  setIndependent_isAtom : CompleteLattice.SetIndependent {I : LieIdeal R L | IsAtom I}
+  sSupIndep_isAtom : sSupIndep {I : LieIdeal R L | IsAtom I}
   /-- In a semisimple Lie algebra, the atoms are non-abelian. -/
   non_abelian_of_isAtom : ∀ I : LieIdeal R L, IsAtom I → ¬ IsLieAbelian I
 

Mathlib/Algebra/Lie/Submodule.lean

@@ -514,9 +514,12 @@ theorem isCompl_iff_coe_toSubmodule :
     IsCompl N N' ↔ IsCompl (N : Submodule R M) (N' : Submodule R M) := by
   simp only [isCompl_iff, disjoint_iff_coe_toSubmodule, codisjoint_iff_coe_toSubmodule]
 
-theorem independent_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
-    CompleteLattice.Independent N ↔ CompleteLattice.Independent fun i ↦ (N i : Submodule R M) := by
-  simp [CompleteLattice.independent_def, disjoint_iff_coe_toSubmodule]
+theorem iSupIndep_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
+    iSupIndep N ↔ iSupIndep fun i ↦ (N i : Submodule R M) := by
+  simp [iSupIndep_def, disjoint_iff_coe_toSubmodule]
+
+@[deprecated (since := "2024-11-24")]
+alias independent_iff_coe_toSubmodule := iSupIndep_iff_coe_toSubmodule
 
 theorem iSup_eq_top_iff_coe_toSubmodule {ι : Sort*} {N : ι → LieSubmodule R L M} :
     ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ := by