Commit 2025-02-21 21:53 8d0660f3

View on Github →

feat: basic structural lemmas about finite crystallographic root pairings. (#21932)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.neg_coroot_mem

added theorem RootPairing.neg_mem_range_coroot_iff

added theorem RootPairing.neg_mem_range_root_iff

added theorem RootPairing.neg_root_mem

added theorem RootPairing.pairingIn_reflection_perm_self_left

added theorem RootPairing.pairingIn_reflection_perm_self_right

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

deleted theorem RootPairing.coxeterWeightIn_le_four

deleted theorem RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic

deleted theorem RootPairing.coxeterWeight_mem_set_of_isCrystallographic

modified theorem RootPairing.exists_ge_zero_eq_rootForm

modified def RootPairing.posRootForm

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

added theorem RootPairing.coxeterWeightIn_eq_zero_iff

added theorem RootPairing.coxeterWeightIn_le_four

added theorem RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic

added theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic

added theorem RootPairing.root_add_root_mem_of_pairingIn_neg

added theorem RootPairing.root_sub_root_mem_of_pairingIn_pos

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

added theorem RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent

added theorem RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four

added theorem RootPairing.pairingIn_neg_one_neg_four_iff

added theorem RootPairing.pairingIn_neg_two_neg_two_iff

added theorem RootPairing.pairingIn_one_four_iff

added theorem RootPairing.pairingIn_two_two_iff

Modified Mathlib/NumberTheory/Divisors.lean

added theorem Int.divisorsAntidiagonal_four

added theorem Int.divisorsAntidiagonal_one

added theorem Int.divisorsAntidiagonal_three

added theorem Int.divisorsAntidiagonal_two

added theorem Int.mul_mem_one_two_three_iff

added theorem Int.mul_mem_zero_one_two_three_four_iff