Skip to content

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

Closed
YaelDillies wants to merge 2 commits intomasterfrom
ssup_indep
Closed

[Merged by Bors] - chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep#19409
YaelDillies wants to merge 2 commits intomasterfrom
ssup_indep

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Nov 23, 2024

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

Open in Gitpod

@YaelDillies YaelDillies added WIP Work in progress t-order Order theory labels Nov 23, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 23, 2024 •
edited
Loading

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).

@YaelDillies
chore: rename CompleteLattice.Independent/.SetIndependent to `iSu…
291655f 
…pIndep`/`sSupIndep`

These names are shorter, closer to `SupIndep` and clearer without their namespace.
@YaelDillies
deprecated aliases
26d2dba
@YaelDillies YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Nov 24, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 24, 2024
jcommelin
jcommelin reviewed Nov 25, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 25, 2024
@YaelDillies
chore: rename CompleteLattice.Independent/.SetIndependent to `iSu…
725d2de 
…pIndep`/`sSupIndep` (#19409)

These names are shorter, closer to `SupIndep` and clearer without their namespace.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep [Merged by Bors] - chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep Nov 25, 2024
@mathlib-bors mathlib-bors bot closed this Nov 25, 2024
@mathlib-bors mathlib-bors bot deleted the ssup_indep branch November 25, 2024 11:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@YaelDillies @jcommelin