Commit 2025-10-27 20:01 0f4d3c56

feat(Order): lemmas about iSupIndep (#29791)

• generalize Finset.SupIndep "bind" operations from DistribLattice to IsModularLattice
• new lemma iSupIndep.iInf
• more characterizations of iSupIndep on submodules:
  • iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero
  • iSupIndep_iff_finset_sum_eq_imp_eq
• add @[simp] and @[grind] attributes which were helpful for these proofs Original motivation was to have the following fact:

theorem iSupIndep_iInf_genEigenspace [NoZeroSMulDivisors R M] {α : Type*} (f : α → End R M)
    (k : ℕ∞) : iSupIndep fun μ : α → R ↦ ⨅ a : α, ((f a).genEigenspace (μ a)) k :=
  .iInf (f · |>.genEigenspace · k) (f · |>.independent_genEigenspace k)