Commit 2025-05-01 22:01 820df42e

View on Github →

feat: add supporting API for Geck's final root system lemma (#24476) 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.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.root_ne_neg_of_ne

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

added theorem RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx

deleted theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le

added theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le_three

added theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le_two

deleted theorem RootPairing.chainBotCoeff_of_not_linInd

added theorem RootPairing.chainBotCoeff_of_not_linearIndependent

added theorem RootPairing.chainBotCoeff_reflection_perm_left

added theorem RootPairing.chainBotCoeff_reflection_perm_right

deleted theorem RootPairing.chainBotCoeff_relfection_perm

deleted theorem RootPairing.chainTopCoeff_of_not_linInd

added theorem RootPairing.chainTopCoeff_of_not_linearIndependent

added theorem RootPairing.chainTopCoeff_reflection_perm_left

added theorem RootPairing.chainTopCoeff_reflection_perm_right

deleted theorem RootPairing.chainTopCoeff_relfection_perm

deleted theorem RootPairing.setOf_root_add_zsmul_eq_Icc_of_linInd

added theorem RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.pairing_eq_zero_iff'

added theorem RootPairing.pairing_eq_zero_iff

deleted theorem RootPairing.pairing_zero_iff'

deleted theorem RootPairing.pairing_zero_iff

added theorem RootPairing.zero_nmem_range_coroot

added theorem RootPairing.zero_nmem_range_root

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

added theorem RootPairing.pairingIn_le_zero_iff

added theorem RootPairing.pairingIn_lt_zero_iff

modified theorem RootPairing.zero_lt_pairingIn_iff'

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

added theorem RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq

added theorem RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_nmem

added theorem RootPairing.forall_pairingIn_eq_swap_or

added theorem RootPairing.forall_pairing_eq_swap_or

modified theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'

modified theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed

modified theorem RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_of_ne

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

deleted theorem RootPairing.pairingIn_zero_iff

Modified Mathlib/LinearAlgebra/RootSystem/Finite/g2.lean

added theorem RootPairing.IsG2.pairingIn_mem_zero_one_three

added theorem RootPairing.isG2_iff

added theorem RootPairing.isNotG2_iff

added theorem RootPairing.not_isG2_iff_isNotG2

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.corootSpanMem_reflection_perm_self

added theorem RootPairing.pairingIn_eq_zero_iff

added theorem RootPairing.rootSpanMem_reflection_perm_self

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

deleted theorem RootPairing.infinite_of_linInd_coxeterWeight_four

added theorem RootPairing.infinite_of_linearIndependent_coxeterWeight_four

added theorem RootPairing.linearIndependent_of_add_mem_range_root

added theorem RootPairing.linearIndependent_of_sub_mem_range_root

deleted theorem RootPairing.pairing_smul_root_eq_of_not_linInd

added theorem RootPairing.pairing_smul_root_eq_of_not_linearIndependent

added theorem RootPairing.two_smul_nmem_range_root

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

added theorem RootPairing.RootPositiveForm.algebraMap_rootLength

added theorem RootPairing.RootPositiveForm.pairingIn_mul_eq_pairingIn_mul_swap

added def RootPairing.RootPositiveForm.rootLength

added theorem RootPairing.RootPositiveForm.rootLength_pos

added theorem RootPairing.RootPositiveForm.rootLength_reflection_perm_self

modified theorem RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff

modified theorem RootPairing.coxeterWeight_nonneg

modified theorem RootPairing.zero_lt_pairingIn_iff