Commit 2025-04-07 18:17 fa4b09af

View on Github →

feat: a finite crystallographic reduced irreducible root pairing containing two roots with Coxeter weight three is spanned by this pair (#23634)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

modified theorem Submodule.mem_invtSubmodule_reflection_of_mem

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

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

added theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'

added theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed

deleted theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic_of_isReduced

added theorem RootPairing.pairingIn_pairingIn_mem_set_of_length_eq

added theorem RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_of_ne

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

added theorem RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs

added theorem RootPairing.EmbeddedG2.allRoots_nodup

added theorem RootPairing.EmbeddedG2.allRoots_subset_range_root

added theorem RootPairing.EmbeddedG2.card_index_eq_twelve

added def RootPairing.EmbeddedG2.indexEquivAllRoots

added theorem RootPairing.EmbeddedG2.isOrthogonal_short_and_long

added theorem RootPairing.EmbeddedG2.linearIndependent_short_long

added theorem RootPairing.EmbeddedG2.long_eq_three_mul_short

added theorem RootPairing.EmbeddedG2.mem_allRoots

added theorem RootPairing.EmbeddedG2.mem_span_of_mem_allRoots

added def RootPairing.EmbeddedG2.ofPairingInThree

added theorem RootPairing.EmbeddedG2.pairingIn_shortAddLong_left

added theorem RootPairing.EmbeddedG2.pairingIn_shortAddLong_right

added theorem RootPairing.EmbeddedG2.pairingIn_short_long

added theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_left

added theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_right

added theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_left

added theorem RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_right

added theorem RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_left

added theorem RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_right

added theorem RootPairing.EmbeddedG2.pairing_long_short

added theorem RootPairing.EmbeddedG2.pairing_short_long

added theorem RootPairing.EmbeddedG2.setOf_index_eq_univ

added def RootPairing.EmbeddedG2.shortAddLong

added theorem RootPairing.EmbeddedG2.shortAddLongRoot_eq

added theorem RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot

added theorem RootPairing.EmbeddedG2.span_eq_top

added def RootPairing.EmbeddedG2.threeShortAddLong

added theorem RootPairing.EmbeddedG2.threeShortAddLongRoot_eq

added theorem RootPairing.EmbeddedG2.threeShortAddLongRoot_longRoot

added def RootPairing.EmbeddedG2.threeShortAddTwoLong

added theorem RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_eq

added theorem RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot

added def RootPairing.EmbeddedG2.twoShortAddLong

added theorem RootPairing.EmbeddedG2.twoShortAddLongRoot_eq

added theorem RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

modified theorem RootPairing.span_root_image_eq_top_of_forall_orthogonal

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

added theorem RootPairing.InvariantForm.isOrthogonal_iff_pairing_eq_zero

Modified Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean

added def RootPairing.weylGroup.ofIdx

added theorem RootPairing.weylGroup.ofIdx_smul