Commit 2024-08-19 19:49 be86c993

View on Github →

feat (LinearAlgebra/RootSystem/Defs): define Weyl group (#15702) This PR defines the Weyl group of a root pairing, and its permutation representation on the indexing set of roots.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

added theorem Subgroup.smul_mem_of_mem_closure_of_mem

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coreflection_inv

added theorem RootPairing.coreflection_sq

added theorem RootPairing.exists_root_eq_smul_of_mem_weylGroup

added theorem RootPairing.mem_range_coroot_of_mem_range_coreflection_of_mem_range_coroot

added theorem RootPairing.mem_range_root_of_mem_range_reflection_of_mem_range_root

added theorem RootPairing.pairing_smul_coroot_eq

added theorem RootPairing.pairing_smul_root_eq

added theorem RootPairing.range_weylGroupToPerm

added theorem RootPairing.reflection_inv

added theorem RootPairing.reflection_mem_weylGroup

added theorem RootPairing.reflection_perm_eq_reflection_perm_iff_of_isSMulRegular

added theorem RootPairing.reflection_perm_eq_reflection_perm_iff_of_span

added theorem RootPairing.reflection_perm_inv

added theorem RootPairing.reflection_perm_sq

added theorem RootPairing.reflection_sq

added theorem RootPairing.two_nsmul_reflection_eq_of_perm_eq

added def RootPairing.weylGroup

added def RootPairing.weylGroupToPerm

added theorem RootPairing.weylGroupToPerm_apply_reflection

added theorem RootSystem.reflection_perm_eq_reflection_perm_iff