[Merged by Bors] - feat: linear independence of indecomposable roots of a root system

[ocfnash]

---

Work toward #28717

[github-actions]

PR summary 0bf098cae7

Import changes exceeding 2%

%	File
+59.21%	Mathlib.Algebra.Group.Irreducible.Indecomposable

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Irreducible.Indecomposable	304	484	+180 (+59.21%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Group.Irreducible.Indecomposable	180
Mathlib.LinearAlgebra.RootSystem.BaseExists (new file)	1433

---

Declarations diff

+ IsMulIndecomposable.baseOf
+ IsMulIndecomposable.baseOf_subset_one_lt
+ IsMulIndecomposable.image_baseOf_inv_comp_eq
+ IsMulIndecomposable.subset
+ Subgroup.closure_image_isMulIndecomposable_baseOf
+ Submonoid.closure_image_isMulIndecomposable_baseOf
+ algebraMap_pairingIn'
+ baseOf_pairwise_pairing_le_zero
+ invMonoidHom_comp_invMonoidHom
+ linearIndepOn_root_baseOf
+ linearIndepOn_root_baseOf'
+ mem_or_inv_mem_closure_baseOf
+ pairwise_baseOf_div_notMem
+ pairwise_div_notMem_range
+ pairwise_div_notMem_range'
+ posForm_apply_root_root_le_zero_iff
- Submonoid.closure_image_one_lt_and_isMulIndecomposable

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:

• Lint style
• Build
• Post-Build Step