Mathlib Changelog
v4
Changelog
About
Github
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