Commit 2025-02-26 10:06 514991a1

View on Github →

feat: more structural lemmas about root pairings (#22213) The main results are:

RootPairing.Base.cartanMatrix_le_zero_of_ne (off-diagonal entries of Cartan matrices are non-positive)
RootPairing.Base.root_sub_root_mem_of_mem_of_mem (lemma 2.5 from Geck 2017)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem Fintype.mem_span_image_iff_exists_fun

added theorem mem_span_image_iff_exists_fun

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

deleted theorem LinearIndependent.restrict_scalars_algebras

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndependent.restrict_scalars'

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.pos_or_neg_of_sum_smul_root_mem

added theorem RootPairing.Base.sub_nmem_range_coroot

added theorem RootPairing.Base.sub_nmem_range_root

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

modified theorem RootPairing.Base.cartanMatrixIn_apply_same

added theorem RootPairing.Base.cartanMatrix_apply_same

added theorem RootPairing.Base.cartanMatrix_le_zero_of_ne

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

modified theorem RootPairing.exists_ge_zero_eq_rootForm

added theorem RootPairing.pairingIn_zero_iff

modified def RootPairing.posRootForm

added theorem RootPairing.zero_lt_pairingIn_iff'

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

added theorem RootPairing.Base.pairingIn_le_zero_of_ne

added theorem RootPairing.Base.root_add_root_mem_of_mem_of_mem

added theorem RootPairing.Base.root_sub_root_mem_of_mem_of_mem

modified theorem RootPairing.root_add_root_mem_of_pairingIn_neg

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified docs/references.bib