[Merged by Bors] - chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep

[YaelDillies]

These names are shorter, closer to SupIndep and clearer without their namespace.

---

[github-actions]

PR summary 26d2dba6de

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ CompleteLattice.Independent
+ CompleteLattice.Independent.comp
+ CompleteLattice.Independent.comp'
+ CompleteLattice.Independent.disjoint_biSup
+ CompleteLattice.Independent.injOn
+ CompleteLattice.Independent.injective
+ CompleteLattice.Independent.map_orderIso
+ CompleteLattice.Independent.mono
+ CompleteLattice.Independent.pairwiseDisjoint
+ CompleteLattice.Independent.setIndependent_range
+ CompleteLattice.SetIndependent
+ CompleteLattice.SetIndependent.disjoint_sSup
+ CompleteLattice.SetIndependent.mono
+ CompleteLattice.SetIndependent.pairwiseDisjoint
+ CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent
+ CompleteLattice.WellFoundedGT.finite_of_independent
+ CompleteLattice.WellFoundedGT.finite_of_setIndependent
+ CompleteLattice.WellFoundedLT.finite_ne_bot_of_independent
+ CompleteLattice.WellFoundedLT.finite_of_independent
+ CompleteLattice.WellFoundedLT.finite_of_setIndependent
+ CompleteLattice.independent_def
+ CompleteLattice.independent_def'
+ CompleteLattice.independent_def''
+ CompleteLattice.independent_empty
+ CompleteLattice.independent_map_orderIso_iff
+ CompleteLattice.independent_ne_bot_iff_independent
+ CompleteLattice.independent_of_independent_coe_Iic_comp
+ CompleteLattice.independent_pair
+ CompleteLattice.independent_pempty
+ CompleteLattice.setIndependent_empty
+ CompleteLattice.setIndependent_iff
+ CompleteLattice.setIndependent_pair
+ CompleteLattice.setIndependent_singleton
+ Finset.SupIndep.iSupIndep_of_univ
+ IsInternal.addSubgroup_iSupIndep
+ IsInternal.addSubmonoid_iSupIndep
+ IsInternal.submodule_iSupIndep
+ LinearIndependent.iSupIndep_span_singleton
+ Submodule.finite_ne_bot_of_iSupIndep
+ WellFoundedGT.finite_ne_bot_of_iSupIndep
+ WellFoundedGT.finite_of_iSupIndep
+ WellFoundedGT.finite_of_sSupIndep
+ WellFoundedLT.finite_ne_bot_of_iSupIndep
+ WellFoundedLT.finite_of_iSupIndep
+ WellFoundedLT.finite_of_sSupIndep
+ _root_.Set.PairwiseDisjoint.sSupIndep
+ eigenspaces_iSupIndep
+ eq_one_of_noncommProd_eq_one_of_iSupIndep
+ exists_sSupIndep_isCompl_sSup_atoms
+ exists_sSupIndep_of_sSup_atoms_eq_top
+ exists_sSupIndep_sSup_simples_eq_top
+ iSupIndep
+ iSupIndep.comp
+ iSupIndep.comp'
+ iSupIndep.dfinsupp_lsum_injective
+ iSupIndep.dfinsupp_sumAddHom_injective
+ iSupIndep.disjoint_biSup
+ iSupIndep.fintypeNeBotOfFiniteDimensional
+ iSupIndep.injOn
+ iSupIndep.injective
+ iSupIndep.linearIndependent
+ iSupIndep.linearIndependent'
+ iSupIndep.map_orderIso
+ iSupIndep.mono
+ iSupIndep.of_coe_Iic_comp
+ iSupIndep.pairwiseDisjoint
+ iSupIndep.sSupIndep_range
+ iSupIndep.subtype_ne_bot_le_finrank
+ iSupIndep.subtype_ne_bot_le_finrank_aux
+ iSupIndep.subtype_ne_bot_le_rank
+ iSupIndep.supIndep
+ iSupIndep.supIndep'
+ iSupIndep.sup_indep_univ
+ iSupIndep_def
+ iSupIndep_def'
+ iSupIndep_def''
+ iSupIndep_empty
+ iSupIndep_genWeightSpace
+ iSupIndep_genWeightSpace'
+ iSupIndep_genWeightSpaceOf
+ iSupIndep_iff_coe_toSubmodule
+ iSupIndep_iff_dfinsupp_lsum_injective
+ iSupIndep_iff_dfinsupp_sumAddHom_injective
+ iSupIndep_iff_forall_dfinsupp
+ iSupIndep_iff_linearIndependent_of_ne_zero
+ iSupIndep_iff_pairwiseDisjoint
+ iSupIndep_iff_supIndep
+ iSupIndep_iff_supIndep_of_injOn
+ iSupIndep_iff_supIndep_univ
+ iSupIndep_map_orderIso_iff
+ iSupIndep_ne_bot
+ iSupIndep_of_dfinsupp_lsum_injective
+ iSupIndep_of_dfinsupp_sumAddHom_injective
+ iSupIndep_of_dfinsupp_sumAddHom_injective'
+ iSupIndep_pair
+ iSupIndep_pempty
+ iSupIndep_sUnion_of_directed
+ independent_iff_iSupIndep
+ isInternal_biSup_submodule_of_iSupIndep
+ isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
+ isInternal_submodule_of_iSupIndep_of_iSup_eq_top
+ sSupIndep
+ sSupIndep.disjoint_sSup
+ sSupIndep.mono
+ sSupIndep.pairwiseDisjoint
+ sSupIndep_empty
+ sSupIndep_iUnion_of_directed
+ sSupIndep_iff
+ sSupIndep_iff_finite
+ sSupIndep_iff_pairwiseDisjoint
+ sSupIndep_pair
+ sSupIndep_singleton
++ injective_noncommPiCoprod_of_iSupIndep
+-- injective_noncommPiCoprod_of_independent
- CompleteLattice.Independent.fintypeNeBotOfFiniteDimensional
- CompleteLattice.Independent.subtype_ne_bot_le_finrank
- CompleteLattice.Independent.subtype_ne_bot_le_finrank_aux
- CompleteLattice.Independent.supIndep
- CompleteLattice.Independent.sup_indep_univ
- Finset.SupIndep.independent_of_univ
- Independent
- Independent.comp
- Independent.comp'
- Independent.disjoint_biSup
- Independent.injOn
- Independent.injective
- Independent.map_orderIso
- Independent.mono
- Independent.pairwiseDisjoint
- Independent.setIndependent_range
- SetIndependent
- SetIndependent.disjoint_sSup
- SetIndependent.mono
- SetIndependent.pairwiseDisjoint
- WellFoundedGT.finite_ne_bot_of_independent
- WellFoundedGT.finite_of_independent
- WellFoundedGT.finite_of_setIndependent
- WellFoundedLT.finite_ne_bot_of_independent
- WellFoundedLT.finite_of_independent
- WellFoundedLT.finite_of_setIndependent
- _root_.Set.PairwiseDisjoint.setIndependent
- independent_def
- independent_def'
- independent_def''
- independent_empty
- independent_map_orderIso_iff
- independent_ne_bot_iff_independent
- independent_of_independent_coe_Iic_comp
- independent_pair
- independent_pempty
- setIndependent_empty
- setIndependent_iff
- setIndependent_pair
- setIndependent_singleton

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style