[Merged by Bors] - feat: add supporting API for Geck's final root system lemma

[ocfnash]

Most of this API is to support a proof of Lemma 2.6 from Geck which will be added in a follow-up PR. However these results all make sense in their own right.

---

[github-actions]

PR summary ee6545aa58

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.RootSystem.Chain	1510	1511	+1 (+0.07%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.RootSystem.Chain	1

---

Declarations diff

+ IsG2
+ IsG2.pairingIn_mem_zero_one_three
+ IsNotG2
+ RootPositiveForm.rootLength_le_of_pairingIn_eq
+ RootPositiveForm.rootLength_lt_of_pairingIn_nmem
+ algebraMap_rootLength
+ chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx
+ chainBotCoeff_add_chainTopCoeff_le_three
+ chainBotCoeff_add_chainTopCoeff_le_two
+ chainBotCoeff_of_not_linearIndependent
+ chainBotCoeff_reflection_perm_left
+ chainBotCoeff_reflection_perm_right
+ chainTopCoeff_of_not_linearIndependent
+ chainTopCoeff_reflection_perm_left
+ chainTopCoeff_reflection_perm_right
+ corootSpanMem_reflection_perm_self
+ forall_pairingIn_eq_swap_or
+ forall_pairing_eq_swap_or
+ infinite_of_linearIndependent_coxeterWeight_four
+ instance [P.IsIrreducible] : P.IsG2
+ isG2_iff
+ isNotG2_iff
+ linearIndependent_of_add_mem_range_root
+ linearIndependent_of_sub_mem_range_root
+ not_isG2_iff_isNotG2
+ pairingIn_eq_zero_iff
+ pairingIn_le_zero_iff
+ pairingIn_lt_zero_iff
+ pairingIn_mul_eq_pairingIn_mul_swap
+ pairing_eq_zero_iff
+ pairing_eq_zero_iff'
+ pairing_smul_root_eq_of_not_linearIndependent
+ rootLength
+ rootLength_pos
+ rootLength_reflection_perm_self
+ rootSpanMem_reflection_perm_self
+ root_ne_neg_of_ne
+ setOf_root_add_zsmul_eq_Icc_of_linearIndependent
+ two_smul_nmem_range_root
+ zero_nmem_range_coroot
+ zero_nmem_range_root
- chainBotCoeff_add_chainTopCoeff_le
- chainBotCoeff_of_not_linInd
- chainBotCoeff_relfection_perm
- chainTopCoeff_of_not_linInd
- chainTopCoeff_relfection_perm
- infinite_of_linInd_coxeterWeight_four
- pairingIn_zero_iff
- pairing_smul_root_eq_of_not_linInd
- pairing_zero_iff
- pairing_zero_iff'
- setOf_root_add_zsmul_eq_Icc_of_linInd

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

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[jcommelin]

LGTM, modulo a typo

bors d+

[mathlib-bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style